Lists of fixed length and type literals

ghc, haskell, type-inference

Solution

This is not really an answer.

Using https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2 , this

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits

data List (n :: Nat) a where
  Nil :: List 0 a
  (:>) :: a -> List n a -> List (n+1) a

append :: List n1 a -> List n2 a -> List (n1 + n2) a
append Nil       ys = ys
append (x :> xs) ys = x :> (append xs ys)

... compiles, so obviously it's correct.

Problem

I'm trying to define a type for lists of fixed length in Haskell. When I use the standard way to encode natural numbers as types in unary, everything works fine. However, when I try to build everything on GHC's type literals, I run into tons of problems. My first shot at the desired list type was ``` data List (n :: Nat) a where Nil :: List 0 a (:>) :: a -> List n a -> List (n+1) a ``` which unfortunately didn't allow for writing a zip function with type ``` zip :: List n a -> List n b -> List n (a,b) ``` I could solve this problem by subtracting 1 from the type variable `n` in the type of `(:>)`: ``` data List (n :: Nat) a where Nil :: List 0 a (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's ``` Next, I tried to define an append function: ``` append :: List n1 a -> List n2 a -> List (n1 + n2) a append Nil ys = ys append (x :> xs) ys = x :> (append xs ys) ``` Unfortunately, GHC tells me ``` Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’ ``` Adding the constraint `((n1 + n2) - 1) ~ ((n1 - 1) + n2)` to the signature doesn't solve the problems since GHC complains ``` Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1)) from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2)) ``` Now, I'm obviously caught in some kind of infinite loop. So, I'd like to know if it is possible to define a type for lists of fixed length using type literals at all. Did I perhaps even oversee a library for precisely this purpose? Basically, the only requirement is that I want to write something like `List 3 a` instead of `List (S (S (S Z))) a`.

Original source