Types
gist.github.com
Types
1–10 of 198 posts
Re: Types
#2Hope this makes it into Wikipedia instead of here.
Re: Types
#3The 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 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?
Re: Types
#4The 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…
not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.
Re: Types
#5The 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…
I do NOT know anything about Idris, but I'd imagine you have to do a check along the line of `if (x<y) then` before being able to call `add`, within that block-scope, the compiler should be able to infer that x<y. Typescript has something similar, where if you do `if (foo)`, the compiler will know that foo can't be null or undefined.
Re: Types
#6The 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 whatever kind of application-specific error is appropriate (assuming x > y is some kind of erroneous condition).
Re: Types
#7The 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…
though the comparator cannot return just a boolean, because it could be 'wrong'. this is where the dependent constructs come in to make sure the answer is correct
Re: Types
#8I think types can be both frustrating and life-saving.
However, the "danger" for me lies primarily in implicit conversion. That is, Python vs Lua/JS/R. When writing large programs, some things happen implicitly and linting may not catch it.
Everything else besides implicit conversion just helps structure the programs in specific ways and helps speed them up.
Re: Types
#9Hope this makes it into Wikipedia instead of here.
It'll get moderated out.