Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Types

gist.github.com

Post reply on HN
Print view View original

11–20 of 198 posts

Re: Types

#11

Post by seanwilson »

Great overview article but I have a comment.

> In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument":

> If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time.

> Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.

I really wish when people talk about dependently typed programming languages (e.g. Idris, Coq, Agda, ATS), they would mention the effort involved to get these compile time checks to happen.

These languages allow you to capture almost any program property you can think of as a type. Instead of being limited to saying function F "returns a number/list/string" like common type systems, you can capture arbitrarily complex properties like "F returns an even number", "F returns a permutation of the input list", "F always halts" or "F returns a proof of Fermat's Last Theorem". You don't get this for free and you have to help the computer verify these.

Proving F matches the type is arbitrary hard and is impossible to automated in general (e.g. the halting problem tells us we cannot always tell if a function halts). For example, consider the type "F returns a sorted permutation of the input list", where F could be an implementation of bubble sort, quicksort, merge sort, radix sort or something even more complex. Each algorithm will require a different and potentially complex proof and most of the time the programmer needs to help the computer find the proof. It's completely unlike what people are used to from type systems and is an even more massive leap than for someone moving from the type systems of e.g. C++/Java to Haskell.

I'm glad people are more aware of dependently typed languages but I feel the immense jump in how practical they are to use is severely overlooked.

Re: Types

#12

Post by [deleted] »

_ibu9 wrote: post #6
twblalock wrote: post #3

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The use…

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal what…

[deleted]

Re: Types

#13

Post by twblalock »

_ibu9 wrote: post #6
twblalock wrote: post #3

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The use…

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal what…

What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

Re: Types

#14

Post by seanwilson »

twblalock wrote: post #3

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The use…

> That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?

Before you could call "add", you would have to add a branch/condition to verify "x" and "y" met the pre-conditions. The compiler would then know from the context of where you called "add" that the pre-conditions were always met. As you couldn't guarantee the pre-conditions were always met, you would have a code branch that decides what to do when the pre-conditions aren't satisfied.

The important difference to other languages though is that the compiler enforces that you're never allowed to call "add" unless you know the inputs satisfy the pre-conditions.

Re: Types

#15

Post by NhanH »

The article is mainly focused on static typing. I guess it makes sense since the title is "Types". Although reading this, you might just think that dynamic typing is good for nothing.

The more practical part of the article is great. However, the theoretical part could use some works. Especially the terminology isn't actually clear.

Takes some example, what is "memory-safe" ? The only example makes it sounds like bound checking. And what does "no way to escape the language's type rules" mean? There are some usages of "valid program" and "invalid program" that makes my spider sense tingling as well.

> However, no dynamic language can match the speed of carefully written static code in a language like Rust.

> Any blanket statement of the form "static languages are better at x than dynamic languages" is almost certainly nonsense.

Those two quoted statements come from the article.

The section "Arguments for static and dynamic types" didn't mention a single reason why dynamic typing could be preferable over static-typing. It could at least have mentioned macro, or hand-waving claim that dynamic typing makes for prettier code at time (I think the author of python's requests library made that argument in one of the blog post).

I think the last part should be removed (ranking the language by their typed system power).

> There's a clear trend toward more powerful systems over time, especially when judging by language popularity rather than languages simply existing.

Well, it looks true since we didn't consider any dynamic language at all...

Focusing more on the "Concrete examples of type system power differences" would have been better for the article, I think. Something along the line of an example of Non-nullable type with something simple in TS, to optional/maybe monad, then dependent type that you can implement matrix multiplication (m * n) with (n * p) and got the type (m * p) back.

Re: Types

#16

Post by continuational »

seanwilson wrote: post #11

Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no e…

To some degree, you can choose what you want to prove about your algorithms in those languages.

It's perfectly possible to implement a sorting algorithm without proving that it actually sorts the input, or indeed returns a permutation of the input list at all.

In that sense, you can choose how much efford you want to put into it.

Re: Types

#17

Post by seanwilson »

twblalock wrote: post #13
_ibu9 wrote: post #6

Earlier quoted context omitted.

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal what…

What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

> What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

It would be a type error. All the compiler would know is that "x" and "y" are strings/integers so it would tell you they were the wrong type. If you do a branch on checking they are the correct type, then in that part of the branch the compiler will know they are the correct type and allow "add" to be called.

Think about a Java program that takes a string input, converts the string input to an integer type and then passes this to a function that accepts integers only. If you just tried to pass the string to the function directly the compiler wouldn't allow it. Same thing but the type system is more expressive.

Re: Types

#18

Post by continuational »

twblalock wrote: post #3

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The use…

x = readFromStdin

y = readFromStdin

if(x // in this scope, you have proven x } else {

// in this scope, you have proven x >= y

}

Re: Types

#19

Post by doomrobo »

twblalock wrote: post #3

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The use…

x and y do not have to be known at compile time. If I let y be a random Nat, and x be y - 1 (or 0 if y == 0), then I can statically prove that LE x y.

Re: Types

#20

Post by junke » 

    1 + eval(read_from_the_network())
> If we get an integer, that expression is fine; if we get a string, it's not. We can't know what we'll get until we actually run, so we can't statically analyze the type.

> The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constrained in any way, so this effectively removes the type system's ability to help us with code involving eval. Languages with both eval and a type system have to abandon type safety whenever eval is used.

No, you can give EVAL a returning type of any (T) but still make type inference work.

    (+ 1 (eval (read)))
The meaning of a type in SBCL is: if an expression evaluates without error, then its type is .... In other words, the type of the above expression is NUMBER.

There is also a NIL type (bottom) which represent the empty set of values. If a function has a return type of NIL, it means that it does not return a value normally. This is the case for the ERROR function, or the (LOOP) expression.

Post reply on HN