2 ms·
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.
by 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)