3 ms·

> If you're given an Optional that's guaranteed to have a value, it's better to call get and blow up if someone violates this invariant than to silently ignore

> If you're given an Optional that's guaranteed to have a value, it's better to call get and blow up if someone violates this invariant than to silently ignore the invalid input via pattern matching or optional chaining. Nope that's bad programming. If you know the Maybe is always there, PROVE IT! Step 1 to proving anything: Make a proposition. In other words, swap out `Maybe a` for `a`. Then prove it upstream. Maybe at some point you want to crash, but you definitely want to do it at the boundary and not within your function. Writing a function that takes a Maybe but assumes it's there just seems like asking to break things. > a toy example would be that A and B can both be nil, but it also holds that (A == nil) == (B == nil). Isn't this just `Maybe (A, B)`? If you have both sums and products in your type system, these sorts of situations go away. A more complicated example: You have A and B and A, B, or both are non-null. But both are never null at the same time. The way to lift this invariant into your type system (i.e. make a proposition about your program) is: data IOr a b = ILeft a | IRight b | IBoth a b

layoutIfNeeded 8y ago
Let’s say Math.sqrt returns Optional because we haven’t invented complex numbers yet. You’re given an integer between 1 and 10, you square it, and then take the square root. The result is an Optional, but it’s provably non-nil. On the other hand, you can’t prove this within the type system. (unless we’re talking about Idris or coq or whatever exotic crap that noone’s using outside of academia) >If you have both sums and products in your type system, these sorts of situations go away. Like I said, it’s a toy example. If you need a different example, here’s one: A, B, C and D are Optionals, but at most two of them are nil.
- Dylan16807 8y ago
  If you depend on the square root existing, why not have a (very short) positive_sqrt function? > A, B, C and D are Optionals, but at most two of them are nil. That sounds like something that's quite fragile and should either be wrapped up in its own type or not depended on.
- whateveracct 8y ago
  It's quite easy to work with type-system-checked positive numbers outside of academia. I've done it in production in Haskell and made real money ;) You can write a verbose sum-of-products to encode that ABCD example although if it's really true that only two tops can be nil and it can be any combo and they're all disparate type, I'd love to see what real problem that would be about! Seems nuts. Lemme see if I can have some fun and encode it more elegantly than "unrolling the permutations" :)
  - whateveracct 8y ago
    I just winged it and got this. It was an extremely mechanical GADT to write. Once you've seen one correct-by-construction dependent type, you've seen them all. Just follow the north star (Curry-Howard)! {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} module ABCD where import Data.Kind (Type) data N = Z | S N data AtMostN (n :: N) (ts :: [Type]) where AMN_Nil :: forall m. AtMostN m '[] AMN_Pass :: forall t m rest. AtMostN m rest -> AtMostN m (t ': rest) AMN_Cons :: forall t m rest. t -> AtMostN m rest -> AtMostN (S m) (t ': rest) Let's try to have two optional booleans but say that at most one can be present: λ: AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] <interactive>:7:1: error: • Couldn't match type ‘'S m0’ with ‘'Z’ Expected type: AtMostN ('S 'Z) '[Bool, Bool] Actual type: AtMostN ('S ('S m0)) '[Bool, Bool] • In the expression: AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] In an equation for ‘it’: it = AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] The type error requires some interpretation, but it sees that we set two. Note the ('S ('S m0)) We can say at most two are set and now it compiles: λ: AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S (S Z)) '[Bool, Bool] And we can set just one and compile fine as well: λ: AMN_Pass (AMN_Cons False AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] This is a bare-bones example. We can easily add a lot of sugar on top to make it more ergonomic (maybe even custom type errors)

layoutIfNeeded 8y ago

Let’s say Math.sqrt returns Optional because we haven’t invented complex numbers yet. You’re given an integer between 1 and 10, you square it, and then take the square root. The result is an Optional, but it’s provably non-nil. On the other hand, you can’t prove this within the type system. (unless we’re talking about Idris or coq or whatever exotic crap that noone’s using outside of academia) >If you have both sums and products in your type system, these sorts of situations go away. Like I said, it’s a toy example. If you need a different example, here’s one: A, B, C and D are Optionals, but at most two of them are nil.

Dylan16807 8y ago
If you depend on the square root existing, why not have a (very short) positive_sqrt function? > A, B, C and D are Optionals, but at most two of them are nil. That sounds like something that's quite fragile and should either be wrapped up in its own type or not depended on.
whateveracct 8y ago
It's quite easy to work with type-system-checked positive numbers outside of academia. I've done it in production in Haskell and made real money ;) You can write a verbose sum-of-products to encode that ABCD example although if it's really true that only two tops can be nil and it can be any combo and they're all disparate type, I'd love to see what real problem that would be about! Seems nuts. Lemme see if I can have some fun and encode it more elegantly than "unrolling the permutations" :)
- whateveracct 8y ago
  I just winged it and got this. It was an extremely mechanical GADT to write. Once you've seen one correct-by-construction dependent type, you've seen them all. Just follow the north star (Curry-Howard)! {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} module ABCD where import Data.Kind (Type) data N = Z | S N data AtMostN (n :: N) (ts :: [Type]) where AMN_Nil :: forall m. AtMostN m '[] AMN_Pass :: forall t m rest. AtMostN m rest -> AtMostN m (t ': rest) AMN_Cons :: forall t m rest. t -> AtMostN m rest -> AtMostN (S m) (t ': rest) Let's try to have two optional booleans but say that at most one can be present: λ: AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] <interactive>:7:1: error: • Couldn't match type ‘'S m0’ with ‘'Z’ Expected type: AtMostN ('S 'Z) '[Bool, Bool] Actual type: AtMostN ('S ('S m0)) '[Bool, Bool] • In the expression: AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] In an equation for ‘it’: it = AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] The type error requires some interpretation, but it sees that we set two. Note the ('S ('S m0)) We can say at most two are set and now it compiles: λ: AMN_Cons True (AMN_Cons True AMN_Nil) :: AtMostN (S (S Z)) '[Bool, Bool] And we can set just one and compile fine as well: λ: AMN_Pass (AMN_Cons False AMN_Nil) :: AtMostN (S Z) '[Bool, Bool] This is a bare-bones example. We can easily add a lot of sugar on top to make it more ergonomic (maybe even custom type errors)