Type restriction in type declaration

Question

There is famous example of the type level natural numbers:

data Zero
data Succ n

I have a question about desirable restriction when we applying type constructor Succ. For example, if we want to make such restriction in function definition, we can use the class and context, like in this code:

class Nat n where
  toInt :: n -> Int
instance Nat Zero where
  toInt _ = 0
instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: n)

It's impossible to use toInt (undefined :: Succ Int), it's ok.

But how to realize similar restrictions on type level constructions (perhaps with some advanced type extensions)?

For instance, I'd like to permit using of type constructor Succ only with type Zero and with something, like this: Succ (Succ Zero), Succ (Succ (Succ Zero)) and so on. How to avoid such bad example on compile time:

type Test = Succ Int

(for now, there is no compilation error)

P.S.: It is more interesting for me how to create a restriction on the type declaration of the last sample

Answer 1

Nowadays, we use the DataKinds extension:

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}

-- N is a type, but is also a kind now
-- Zero, Succ Zero, ... are values, but are also type-level values of
-- kind N
data N = Zero | Succ N

-- (We could import Proxy the library, instead)
data Proxy (n :: N) = Proxy

-- Now n is restricted to kind N
class Nat (n :: N) where
  toInt :: proxy n -> Int

instance Nat Zero where
  toInt _ = 0
instance (Nat n) => Nat (Succ n) where
  toInt _ = 1 + toInt (undefined :: Proxy n)

We can then use toInt (Proxy :: Proxy (Succ Zero)). Instead, toInt (Proxy :: Proxy (Succ Int)) will raise a kind error, as wanted.

Personally, I would also replace proxies with more modern stuff like AllowAmbiguousTypes and TypeApplications so to remove the unused argument.

{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables,
             AllowAmbiguousTypes, TypeApplications #-}

data N = Zero | Succ N

-- Now n is restricted to kind N
class Nat (n :: N) where
  toInt :: Int

instance Nat Zero where
  toInt = 0
instance (Nat n) => Nat (Succ n) where
  toInt = 1 + toInt @n

Use this as toInt @(Succ Zero). The toInt @n syntax chooses the n in the typeclass. It does not correspond to any value exchanged at runtime, only a type-level argument which exists at compile time.

---

Using

type Foo = Succ Int

also errors out as wanted:

    • Expected kind ‘N’, but ‘Int’ has kind ‘*’
    • In the first argument of ‘Succ’, namely ‘Int’
      In the type ‘Succ Int’
      In the type declaration for ‘Foo’