Dynamically generate Haskell types at runtime?

Question

Can one define a Haskell type at runtime from a given template? Here's what I mean by this. Suppose I need an integer type that is restricted to some range (unknown precisely at compile time). I also want a feature that:

succ 0 = 1
succ 1 = 2
...
succ n = 0

n being unknown at compile time. I could do something like this:

data WrapInt = WrapInt {
        value       :: Int,
        boundary    :: Int
}

wrapInt :: Int -> Int -> WrapInt
wrapInt boundary value = WrapInt value boundary

Now what I would like to have is to preserve the wrapInt function as it is, but to avoid storing the boundary as a value inside WrapInt type. Instead I would like it to be stored somehow in type definition, which of course means that the type would have to be defined dynamically at runtime.

Is it possible to achieve this in Haskell?

Answer 1

The reflection package lets you generate new "local" instances of a typeclass at runtime.

For example, suppose we have the following typeclass of values that can "wrap around":

{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances #-}

import Data.Reflection
import Data.Proxy

class Wrappy w where
   succWrappy :: w -> w

We define this newtype that carries a phantom type parameter:

data WrapInt s = WrapInt { getValue :: Int } deriving Show

An make it an instance of Wrappy:

instance Reifies s Int => Wrappy (WrapInt s) where
    succWrappy w@(WrapInt i) = 
        let bound = reflect w 
        in
        if i == bound
            then WrapInt 0
            else WrapInt (succ i)

The interesting part is the Reifies s Int constraint. It means: "the phantom type s represents a value of type Int at the type level". Users never define an instance for Reifies, this is done by the internal machinery of the reflection package.

So, Reifies s Int => Wrappy (WrapInt s) means: "whenever s represent a value of type Int, we can make WrapInt s an instance of Wrappy".

The reflect function takes a proxy value that matches the phantom type and brings back an actual Int value, which is used when implementing the Wrappy instance.

To actually "assign" a value to the phantom type, we use reify:

-- Auxiliary function to convice the compiler that
-- the phantom type in WrapInt is the same as the one in the proxy
likeProxy :: Proxy s -> WrapInt s -> WrapInt s
likeProxy _ = id

main :: IO ()
main = print $ reify 5 $ \proxy -> 
    getValue $ succWrappy (likeProxy proxy (WrapInt 5))

Notice that the signature of reify forbids the phantom type from escaping the callback, that's why we must unwrap the result with getValue.

See more examples in this answer, on in the reflection GitHub repo.

Answer 2

It's not impossible — just very ugly. We'll need natural numbers

data Nat = Z | S Nat

and bounded natural numbers

data Bounded (n :: Nat) where
    BZ :: Bounded n
    BS :: Bounded n -> Bounded (S n)

Then your function should be something like

succ :: Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go bn where
    go :: Bounded n -> Maybe (Bounded n)
    go = ...

In go we need to

1. map BZ to Nothing, if n is Z (i.e. if a Bounded achieved its maximum and has overflowed)
2. map BZ to Just (BS BZ), if n is not Z (i.e. if a Bounded didn't achieve its maximum).
3. call go recursively for the BS case.

The problem however is that there is no way to get n at the value level. Haskell is not that dependent. The usual hack is to use singletons. Writing it manually

data Natty (n :: Nat) where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

class NATTY (n :: Nat) where
    natty :: Natty n

instance NATTY Z where
    natty = Zy

instance NATTY n => NATTY (S n) where
    natty = Sy natty

Now we can get a value-level representation of n in the Bounded n in go:

succ :: NATTY n => Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go natty bn where
    go :: Natty n -> Bounded n -> Maybe (Bounded n)
    go  Zy      BZ     = Nothing
    go (Sy ny)  BZ     = Just (BS BZ)
    go (Sy ny) (BS bn) = BS <$> go ny bn

And the NATTY type class is used to infer this value automatically.

Some tests:

instance Eq (Bounded n) where
    BZ    == BZ    = True
    BS bn == BS bm = bn == bm
    _     == _     = False

zero :: Bounded (S (S Z))
zero = BZ

one :: Bounded (S (S Z))
one = BS BZ

two :: Bounded (S (S Z))
two = BS (BS BZ)

main = do
    print $ succ zero == zero -- False
    print $ succ zero == one  -- True
    print $ succ one  == two  -- True
    print $ succ two  == zero -- True

The code.

---

Using the singletons library we can define succ as

$(singletons [d| data Nat = Z | S Nat deriving (Eq, Show) |])

data Bounded n where
    BZ :: Bounded n
    BS :: Bounded n -> Bounded (S n)

succ :: SingI n => Bounded n -> Bounded n
succ bn = fromMaybe BZ $ go sing bn where
    go :: Sing n -> Bounded n -> Maybe (Bounded n)
    go  SZ      BZ     = Nothing
    go (SS ny)  BZ     = Just (BS BZ)
    go (SS ny) (BS bn) = BS <$> go ny bn

---

As to lifting runtime stuff to the type level, there are two approaches: CPS and existential types.