Dynamically generate Haskell types at runtime?

Question

Is it possible to determine the Haskell type at runtime from a given template? Here is what I mean. Suppose I need an integer type that is limited to a certain range (unknown exactly at compile time). I also need a function that:

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

n 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 I would like to save the wrapInt function as it is, but not to store it as a value inside WrapInt. Instead, I would like it to be somehow stored in the type definition, which, of course, means that the type must be determined dynamically at runtime.

Can this be achieved in Haskell?

Answer 1

The reflection package allows you to generate new "local" instances of class classes at run time.

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

 {-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances #-} import Data.Reflection import Data.Proxy class Wrappy w where succWrappy :: w -> w 

We define this new type that contains the phantom type parameter:

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

And 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 restriction of Reifies s Int . This means: "The phantom s type represents an Int type value at the type level." Users never define an instance for Reifies ; this is done by the internal mechanism of the reflection package.

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

The reflect function takes a proxy value that matches the phantom type and returns the actual Int value that 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)) 

Note that the reify signature prohibits the phantom type from escaping callback escaping, so we must deploy the result using getValue .

More details in this answer to the reflection of the GitHub repo .

Answer 2

This is not impossible - just very ugly. We need natural numbers

 data Nat = Z | S Nat 

and limited 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

• map BZ to Nothing if n is Z (i.e. if a Bounded reaches its maximum and overflows)
• map BZ to Just (BS BZ) if n not Z (i.e. if a Bounded not reached its maximum).
• calling go recursively for the BS case.

However, the problem is that at the level of values ​​it is impossible to get n . Haskell is not dependent on this. A common hack is using singletons . Manual Recording

 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 representation of level n at the level of the value in 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 a class like NATTY used to output this value automatically.

Some tests:

 instance Eq (Bounded n) where BZ == BZ = True BS bn == BS bm = bn == bm _ == _ = False zero :: Bounded (S (SZ)) zero = BZ one :: Bounded (S (SZ)) one = BS BZ two :: Bounded (S (SZ)) 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 

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 for raising data at the level level, there are two approaches: CPS and existential types .