4 ms·

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 wri

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)

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)