3 ms·

What's a toy problem in this case? Anything where you can replace even part of a dynamic contract seems like a win.

platz 9y ago
> twblalock 468 days ago [-] > 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 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? 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, or x > y. the proof ensures that at compile time you cannot mess this up. in other words, You have to perform the check at runtime, but the results for the check are enforced via a proof that is ensured to be correct at compile time. Connecting the proof the to the type system at compile time is the magic of dependent types > 18 points by platz 468 days ago [-] here's a full code example in Idris: import Data.String -- takes two integers, and a proof that x < y, and yields an integer add : (x : Integer) -> (y : Integer) -> (prf : x < y = True) -> -- require a proof that that x < y Integer add x y prf = x + y main : IO () main = do sx <- getLine -- read string from input sy <- getLine -- read string from input let Just x = parseInteger sx -- assuming int parse is ok, else error let Just y = parseInteger sy -- assuming int parse is ok, else error case decEq (x < y) True of -- decEq constructs a proof if x < y is True Yes prf => print (add x y prf) No => putStrLn "no prf, x is not less than y" lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error When checking argument prf to function Main.add: Type mismatch between x > y = True (Type of prf) and x < y = True (Expected type) there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value. it's either a compile error or it's valid. c.f. https://news.ycombinator.com/item?id=12349384 https://news.ycombinator.com/item?id=12349384
skybrian 9y ago
It may or may not be a win. If the constraint being validated is trivial and the complexity added is substantial then maybe it's not a win? A common example for demonstrating dependent types seems to validating the length of a list, but they don't show how it's useful in a problem where validating the length is important (for example to prevent security issues). Also, a good example would be performing a calculation on external input data (from user input, a file, or a network connection), rather than on a constant, and showing how invalid input is handled.

> twblalock 468 days ago [-] > 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 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? 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, or x > y. the proof ensures that at compile time you cannot mess this up. in other words, You have to perform the check at runtime, but the results for the check are enforced via a proof that is ensured to be correct at compile time. Connecting the proof the to the type system at compile time is the magic of dependent types > 18 points by platz 468 days ago [-] here's a full code example in Idris: import Data.String -- takes two integers, and a proof that x < y, and yields an integer add : (x : Integer) -> (y : Integer) -> (prf : x < y = True) -> -- require a proof that that x < y Integer add x y prf = x + y main : IO () main = do sx <- getLine -- read string from input sy <- getLine -- read string from input let Just x = parseInteger sx -- assuming int parse is ok, else error let Just y = parseInteger sy -- assuming int parse is ok, else error case decEq (x < y) True of -- decEq constructs a proof if x < y is True Yes prf => print (add x y prf) No => putStrLn "no prf, x is not less than y" lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error When checking argument prf to function Main.add: Type mismatch between x > y = True (Type of prf) and x < y = True (Expected type) there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value. it's either a compile error or it's valid. c.f. https://news.ycombinator.com/item?id=12349384 https://news.ycombinator.com/item?id=12349384

skybrian 9y ago

It may or may not be a win. If the constraint being validated is trivial and the complexity added is substantial then maybe it's not a win? A common example for demonstrating dependent types seems to validating the length of a list, but they don't show how it's useful in a problem where validating the length is important (for example to prevent security issues). Also, a good example would be performing a calculation on external input data (from user input, a file, or a network connection), rather than on a constant, and showing how invalid input is handled.