CODEWITHSUNDEEP
haskelltypes
Mike Izbicki
Mike Izbicki

Reputation: 6366

Using Type Nats to create a type level list (having problems adding numbers on the type level)

Just for fun, I wanted to create a Type level list that knows how long it is. Something like this:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import GHC.TypeLits

data family TypeList a (n::Nat)

data instance TypeList a (0) = EmptyList
data instance TypeList a (1) = TL1 a (TypeList a (0))
data instance TypeList a (2) = TL2 a (TypeList a (1))
data instance TypeList a (3) = TL3 a (TypeList a (2))

But, of course I'd like to generalize this to something like:

data instance TypeList a (n)   = TL3 a (TypeList a (n-1))

But this generates an error:

    TypeList.hs:15:53: parse error on input `-'
    Failed, modules loaded: none.

Another attempt:

data instance TypeList a (n+1) = TL3 a (TypeList a (n))

Also generates an error:

    Illegal type synonym family application in instance: n + 1
    In the data instance declaration for `TypeList'

I assume something like this must be possible. It's definitely possible using the notation:

data Zero
data Succ a

But I can't figure it out with the nicer looking version.

Upvotes: 4

Views: 747

Answers (2)

cdk
cdk

Reputation: 6778

The type-level Nat improvements have landed in GHC 7.8 and this is now possible!

{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE TypeFamilies, TypeOperators #-}

import GHC.TypeLits

data family List (n :: Nat) a
data instance List 0 a = Nil
data instance List n a = a ::: List (n - 1) a

infixr 8 :::

using List is just as natural as any []-like data structure you'd write yourself:

λ. :t 'a' ::: 'b' ::: 'c' ::: Nil
'a' ::: 'b' ::: 'c' ::: Nil :: List 3 Char

Upvotes: 6

shachaf
shachaf

Reputation: 8930

As they are in GHC 7.6, type-level Nats won't let you do this sort of thing. There's currently more or less no relation between the types 0 :: Nat and 1 :: Nat, despite what the names suggest (unlike, say, your Zero and Succ Zero, which you can do useful things with). This is going to be better in future versions of GHC.

Upvotes: 3

Related Questions