Re: [Haskell-cafe] induction on type-level Nat

16 Jan 2023

      On Fri, 13 Jan 2023, Henning Thielemann wrote:
...
I want to define a list with type-level Nat length:
type family List (n::Nat) :: Type -> Type where
  List 0 = End
  List n = Cons (List (n-1))
data End a = End
data Cons f a = Cons { head :: a, tail :: f a }
Alternative approach with a GADT:

data T n a where
    End :: T 0 a
    Cons :: a -> T n a -> T (n+1) a

viewL :: T (n+1) a -> (a, T n a)
viewL (Cons x xs) = (x, xs)

testEnd :: T 0 a -> ()
testEnd End = ()

For viewL GHC reports a missing pattern match on 'End' and for testEnd it 
reports a missing match on 'Cons'. If I add the constraint (1<=n+1) to 
Cons then the testEnd warning disappears. If I add the constraint (1<=n+1) 
to viewL, then its warning disappears, as well.