5 ms·

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

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)

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)