create a Haskell type with finitely many inhabitants

Question

According to “Haskell for a great good”, the type declaration for Bool is

data Bool = True | False

and that the type declaration for Int may be considered something like

data Int = -2147483648 | -2147483647 | ... | -1 | 0 | 1 | 2 | ... | 2147483647

For some abstract algebra applications, I would like to create an analogous type with finitely many specified values, for example the values may be integers between $0$ and $n$, for some $n$. Despite the claimed definition of Int, the following doesn’t work:

data F3 = 0 | 1 | 2

with error "Illegal literal in type”. How can I create a type where these are the only inhabitants? Something like:

data F a = (Int a) => [0..a]

would be totally awesome.

Also, can I create a function that enumerates all the valid values of a type, or returns a list of values?

Answer 1

You can use nullary constructors (like True, False, Nothing, () etc)

data F3 = Zero | One | Two
    deriving (Bounded, Enum, Show)

To enumerate all valid values, we simply derive Enum and Bounded and let GHC do all the work for us.

enum :: (Bounded a, Enum a) => [a]
enum = [minBound .. maxBound]

λ. enum :: [F3]
[Zero,One,Two]

If you want to use these like actual Int, you can use fromEnum :: Enum a => a -> Int which will be equivalent to

fromEnum Zero = 0
fromEnum One  = 1
fromEnum Two  = 2

Answer 2

You can't use integer literals in a new type like that. They are already taken, so it isn't valid syntax.

cdk's answer gives a much more practical scenario, but I thought I would give an example of how something like your last example could be implemented in Haskell.

If we turn on some of the more fun extensions, we can convince GHC to make a type with a given finite number of values. I probably wouldn't suggest actually doing this in real code, however, because GHC doesn't have the best support for this kind of dependent type-like programming at the moment. Also, unfortunately, the values don't have nice names. As far as I know, there isn't a way to give them nice names like 1, 2, 3... (edit: actually, we can improve on this a little bit, see the second code block).

It could go something like this:

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

module Fin (Fin (..))
  where

import GHC.TypeLits -- We get Nat from here as well as the type-level `<=` and `+`.

-- This is a type parameterized by another type. The type that parameterizes (`Nat`)
-- behaves like natural numbers at a type level. The `Nat -> *` is the "kind" of the type
-- `Fin`. A kind is like a type for types. To put it another way, a kind is to a type what
-- a type is to a value. In this case, the type `Nat` has kind `Nat`.
data Fin :: Nat -> * where
  FZero :: Fin upperBound
  FSucc :: (1 <= upperBound) => Fin upperBound -> Fin (upperBound + 1)

-- This is ok, because we are using the "fourth" value in a type with five values.
fifthValue :: Fin 5
fifthValue = FSucc (FSucc (FSucc FZero))

-- This doesn't compile, because it tries to make something of type
-- `Fin 2` using a "3rd value".
--    thirdValue :: Fin 2
--    thirdValue = FSucc (FSucc FZero)
--
-- The only inhabitants of `FiniteList 2` are `FZero` and `FSucc FZero`

Note that to actually get instances for things like Eq and Ord you might have to do even more tricky things (I'm not even totally sure if it's possible. It might need the new type level natural number theorem prover that they're putting in GHC 7.10).

One other thing I should probably point out is that the types that inhabit the kind Nat are named 1, 2, .... This is ok because there isn't anything else that use those names at a type level (just at a value level).

Edit:

If we turn on a couple more extensions, we can get a version where you can (almost) directly specify the names of the values:

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators, PolyKinds, TypeFamilies, UndecidableInstances #-}
import Data.Type.Equality
import GHC.TypeLits

type family (||) (a :: Bool) (b :: Bool) :: Bool where
  True  || x  = True
  False || x  = x

type family Elem (a :: k) (xs :: [k]) :: Bool where
  Elem x (y ': ys) = (x == y) || Elem x ys
  Elem x '[]       = False


data NamedFin :: [k] -> * where
  Val :: ((a `Elem` as) ~ True) => Proxy a -> NamedFin as

-- Countdown n makes a type level list of Nats.
-- So, for example, Countdown 3 is a shorthand for '[3, 2, 1]
type family Countdown (a :: Nat) :: [Nat] where
  Countdown 0 = '[]
  Countdown n = (n - 1) ': Countdown (n - 1)

data Proxy a = Proxy deriving Show

type Example = NamedFin (Countdown 5) -- This is the same as NamedFin '[5, 4, 3, 2, 1]

-- This compiles...
example :: Example
example = Val (Proxy :: Proxy 4)

-- ...but this doesn't
--     example2 :: Example
--     example2 = Val (Proxy :: Proxy 10)

There will still be issues making instances for Eq and Ord though.