Equality constraints on type level lists

Question

I'm trying to enforce a type-level constraint that a type-level list must be the same length as a type-level Nat being carried around. For example, using Length from singletons [1] package:

data (n ~ Length ls) => NumList (n :: Nat) (ls :: [*])

test :: Proxy (NumList 2 '[Bool, String, Int])
test = Proxy

I would not expect this code to compile, since there is a mismatch.

EDIT: As dfeuer mentioned Datatype contexts aren't a good idea. I can do the comparison at the value level, but I want to be able to do this at the type level:

class NumListLen a 
  sameLen :: Proxy a -> Bool

instance (KnownNat n, KnownNat (Length m)) => NumListLen (NumList n m) where
  sameLen = const $ (natVal (Proxy :: Proxy n)) == (natVal (Proxy :: Proxy (Length m)))

~~~~

EDIT: Sorta answered my own question, simply add the constraint to the instance:

class NumListLen a 
  sameLen :: Proxy a -> Bool

instance (KnownNat n, KnownNat (Length m), n ~ Length m) => NumListLen (NumList n m) where
  sameLen = const $ (natVal (Proxy :: Proxy n)) == (natVal (Proxy :: Proxy (Length m)))

/home/aistis/Projects/SingTest/SingTest/app/Main.hs:333:13:
    Couldn't match type ‘3’ with ‘2’
    In the second argument of ‘($)’, namely ‘sameLen test’
    In a stmt of a 'do' block: print $ sameLen test
    In the expression:
      do { print $ sameLen test;
           putStrLn "done!" }

[1] https://hackage.haskell.org/package/singletons-2.0.0.2/docs/Data-Promotion-Prelude-List.html#t:Length

That's a datatype context. Datatype contexts are utterly useless. I suspect you're not going to be able to do exactly what you're trying to do in Haskell just yet, but singletons can do some weird stuff.... — dfeuer
Yes, you are right, datatype contexts are not exactly how I would want to do this. But they get the point across. I am able to reify the type value and do the comparison at the value level, but this isn't what I want to do. — Aistis Raulinaitis
Can you explain a bit better what exactly your ultimate goal is here? What do you want to express, really? — dfeuer
I just want to be able to take a type level nat and a type level list and check that n ~ Length ls at the type level, I don't want to do it at the value level. I edited my OP with additional details. — Aistis Raulinaitis
Have you looked at frightening things like Data.Singletons.Prelude.Eq? I don't know what to make of that, but there might well be a simpler way. — dfeuer

user2407038 user2407038 · Accepted Answer · 2016-01-13T08:21:20

If this is something like an invariant (which it seems it is), you should store the proof in the datatype:

{-# LANGUAGE PolyKinds, UndecidableInstances #-} 

import GHC.TypeLits 

type family Length (xs :: [k]) :: Nat where 
  Length '[] = 0 
  Length (x ': xs) = 1 + Length xs 

data TList n l where 
  TList :: (Length xs ~ n) => TList n xs

Note that while the proof is still available at the type level, it is sort of "hidden" behind the data constructor. You can recover the proof simply by pattern matching:

data (:~:) a b where Refl :: a :~: a 

test :: TList n l -> Length l :~: n 
test TList = Refl

Now, mismatches between the two parameters are a type error:

bad :: TList 3 '[Int, Bool]
bad = TList 

good :: TList 2 '[Int, Bool]
good = TList

Of course this can still be beaten by bottom values, so

uh_oh :: TList 10 '[] 
uh_oh = undefined

To avoid this, simply make sure you always pattern match on the TList constructor.

Equality constraints on type level lists

2 Answers