induction on type-level Nat
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 } But this way, GHC cannot match ‘List (n+1)’ with ‘Cons (List n)’, also not with the magic type checker plugings suggested before. I guess I need a another way to define List or some support for the type checker to accept List (n+1) ~ Cons (List n).
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.
On Mon, 16 Jan 2023, Henning Thielemann wrote:
Alternative approach with a GADT:
data T n a where End :: T 0 a Cons :: a -> T n a -> T (n+1) a
...
If I add the constraint (1<=n+1) to Cons then the testEnd warning disappears.
This definition looks less stupid and works, too: data T n a where End :: T 0 a Cons :: (1<=n) => a -> T (n-1) a -> T n a
participants (1)
-
Henning Thielemann