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

See [What is the DataKinds extension of Haskell?](https://stackoverflow.com/questions/20558648/what-is-the-datakinds-extension-of-haskell) for precisely this example. — user11228628, Jun 26 '19 at 17:15

chi · Accepted Answer · 2019-06-28T10:23:42.723

5

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’

edited Jun 28 '19 at 10:23

answered Jun 26 '19 at 17:34

chi

111,837
3
133
218

thanks; just noticed another one: `Proxy` in `class Nat (n :: N) where toInt :: proxy n -> Int`... – Will Ness Jun 27 '19 at 10:56
1

@WillNess No, that's actually a standard idiom (which I don't like, but I conform to). Using the type variable `proxy` instead of the type `Proxy` allows for other proxy types as well. It is often used in [libraries](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Proxy.html#v:asProxyTypeOf) – chi Jun 27 '19 at 11:08
@chi, I am confused, but your first example is not compilable. The second one is wrong: firstly you slightly changed condition. `Succ` is not value constructor as you written, but must be a type constructor. And real error of 2st example is `>:3:12: error: Not in scope: type constructor or class 'Succ'` `A data constructor of that name is in scope; did you mean DataKinds?` – Vladimir Jun 28 '19 at 04:56
I mean for 2nd sample: `Main> type Foo = Succ Int` `:3:12: error:` `Not in scope: type constructor or class 'Succ'` `A data constructor of that name is in scope; did you mean DataKinds?` – Vladimir Jun 28 '19 at 05:03
1

@Vladimir You did not copy all my code in a Haskell, including the line which enables `DataKinds` – chi Jun 28 '19 at 07:24
I've copypasted 1st your sample and have got: C:\_TMP\Haskell\tmp>ghci ans1.hs GHCi, version 8.6.5: [1 of 1] Compiling Main ( ans1.hs, interpreted ) ans1.hs:18:37: error: * Expected a type, but `n' has kind `N' * In an expression type signature: n In the first argument of `toInt', namely `(undefined :: n)' In the second argument of `(+)', namely `toInt (undefined :: n)' | 18 | toInt _ = 1 + toInt (undefined :: n) | ^ Failed, no modules loaded. – Vladimir Jun 28 '19 at 09:40
Second example works as you described if I've put `type Foo = Succ Int` in code file (not in ghci as I did before). But role of `Succ` in your code is not clear for me yet :( – Vladimir Jun 28 '19 at 09:55
@Vladimir I indeed forgot `(undefined :: Proxy n)` in my first snippet, sorry. It should be fixed now. About `Succ`: it plays the same role as in your question. `Succ Int` is an error, since `Succ` wants a number in `N`, and not a type -- this is what you wanted, right? So you can only use `Succ Zero, Succ (Succ Zero), ...`. – chi Jun 28 '19 at 10:26
1

In my code (conditions, if you want) `Succ` is type constructor, but in your code `Succ` looks like data (value) constructor. It confuses me... Perhaps, it is a form of `DataKinds` magic? – Vladimir Jun 28 '19 at 10:52
1

@Vladimir Yes, that's `DataKinds` in action. With that extension, term-level constructors like `Zero, Succ` in my code get "lifted" at the type level. So you can use them as usual in values, but you can also use them in types. The notation `class Nat (n : N)` indicates that `Nat` is not a class of types (we can't use `Nat Bool`) but a class of `N` (we can use `Nat Zero`), so it refers to the lifted values. So we have `Int, Maybe Int, [Int] :: *` as plain types, and `Zero, Succ Zero, ... :: N` as "numbers at the type level". Here `*` and `N` are called "kinds" (a sort of "type of a type"). – chi Jun 28 '19 at 11:56

Type restriction in type declaration

1 Answers1