Type-Level Programming Example
On Reddit, someone asked the following question:
Some time ago, Paczesiowa wrote a comment that claimed:
you can have a function that accepts only prime number of arguments, that are all strings, but occurences of integers at the indixes that are fibonacci numbers
Type-level programming is something that interests me but so far I have only done it in C++. So, here it is in C++, what does it look like in Haskell?
Okay, good question. What does that look like in Haskell? The following code is not pretty. It also gives truly awful error messages. This isn’t a practical technique; it’s just exploring the capabilities of the language for fun.
Edit: Here’s a working version, using techniques demonstrated by jputnam on the Reddit thread. The original code follows.
{-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE Rank2Types #-} module WackyStuff where import Data.List (intercalate) -- for the test function ------------------------------------------------------------------------------- {- Obvious we'll need type-level naturals, so let's build some. -} data Zero data Succ a type SSucc a = Succ (Succ a) type SSSucc a = Succ (SSucc a) type SSSSucc a = Succ (SSSucc a) type SSSSSucc a = Succ (SSSSucc a) type SSSSSSucc a = Succ (SSSSSucc a) type One = Succ Zero type Two = Succ One type Three = Succ Two type Four = Succ Three type Five = Succ Four type Six = Succ Five type Seven = Succ Six type Eight = Succ Seven type Nine = Succ Eight type Ten = Succ Nine ------------------------------------------------------------------------------- {- Arithmetic -} type family a :+: b type instance Zero :+: x = x type instance (Succ x) :+: y = Succ (x :+: y) type family a :*: b type instance Zero :*: x = Zero type instance (Succ x) :*: y = y :+: (x :*: y) -- Subtraction gives 0 if a < b type family a :-: b type instance Zero :-: a = Zero type instance (Succ a) :-: Zero = Succ a type instance (Succ a) :-: (Succ b) = a :-: b -- Division rounds all fractions up. Yeah, that's weird... but it's -- documented, so it's not a bug. :) type family a :/: b type instance Zero :/: b = Zero type instance (Succ a) :/: b = Succ (((Succ a) :-: b) :/: b) ------------------------------------------------------------------------------- {- It's also nice to have some logic operations. -} data HTrue data HFalse type family Or a b type instance Or HFalse HFalse = HFalse type instance Or HFalse HTrue = HTrue type instance Or HTrue HFalse = HTrue type instance Or HTrue HTrue = HTrue type family And a b type instance And HFalse HFalse = HFalse type instance And HFalse HTrue = HFalse type instance And HTrue HFalse = HFalse type instance And HTrue HTrue = HTrue type family Not a type instance Not HFalse = HTrue type instance Not HTrue = HFalse type family NatEq a b type instance NatEq Zero Zero = HTrue type instance NatEq Zero (Succ n) = HFalse type instance NatEq (Succ n) Zero = HFalse type instance NatEq (Succ n) (Succ m) = NatEq n m ------------------------------------------------------------------------------- {- Type level lists. Membership testing depends on the lists containing integers. -} data Cons a b data Nil type family Member elem list type instance Member x Nil = HFalse type instance Member x (Cons a b) = Or (NatEq a x) (Member x b) ------------------------------------------------------------------------------- {- Primality testing. A number is prime if it is not divisible by any number less than itself but greater than one. -} type Divis a b = NatEq a ((a :/: b) :*: b) type family PossibleDivisors n -- Precondition: n > 1 type instance PossibleDivisors Two = Nil type instance PossibleDivisors (SSSucc a) = Cons (SSucc a) (PossibleDivisors (SSucc a)) type family DivisAny a b type instance DivisAny a Nil = HFalse type instance DivisAny a (Cons b c) = Or (Divis a b) (DivisAny a c) type family Prime n type instance Prime Zero = HFalse type instance Prime One = HFalse type instance Prime (SSucc n) = Not (DivisAny (SSucc n) (PossibleDivisors (SSucc n))) ------------------------------------------------------------------------------- {- Fibonacci testing -} type family NFibs n a b type instance NFibs Zero a b = Nil type instance NFibs (Succ n) a b = Cons a (NFibs n b (a :+: b)) type family IsFib n type instance IsFib n = Member n (NFibs (n :+: Two) Zero One) ------------------------------------------------------------------------------- {- Much of the problem deals with the number and indices of parameters to a function, so here we deal with that subtlety. Because of currying, the line between the "parameters" and the "result" types of functions in Haskell are blurred. We draw that line with a newtype wrapper, Result. The piece of the function that ought to be viewed as the result type must be enclosed in the Result type wrapper. -} newtype Result a = Result { unResult :: a } deriving Show type family NumParams f type instance NumParams (Result a) = Zero type instance NumParams (p -> x) = Succ (NumParams x) {- We now define the concept of a function whose fibonacci-numbered parameters are integers, and whose non-fibonacci-numbered parameters are strings. In order to make functions of this form definable, we include a general fold for constructing the values. -} class FibParamed f r where fibfold :: a -> (String -> a -> a) -> (Int -> a -> a) -> (a -> r) -> f instance FibParamed (Result r) r where fibfold a fs fz g = Result (g a) instance (FibParamed f r, IsFib (NumParams f) ~ HTrue) => FibParamed (Int -> f) r where fibfold a fs fz g z = fibfold (fz z a) fs fz g instance (FibParamed f r, IsFib (NumParams f) ~ HFalse) => FibParamed (String -> f) r where fibfold a fs fz g s = fibfold (fs s a) fs fz g {- We now add the condition that the number of parameters is prime, giving us the final type. -} type WackyType r = (FibParamed f r, Prime (NumParams f) ~ HTrue) => f ------------------------------------------------------------------------------- {- Here is the test function, defined in terms of the earlier fold. -} test :: WackyType String test = fibfold [] (flip (++) . (:[])) (flip (++) . (:[]) . show) (intercalate ",") {- And a main function to test it. Note that we do need to be explicit about types here. -} main = do let t1 = unResult (test (5::Int) (6::Int) :: Result String) let t2 = unResult (test "hi" (6::Int) (7::Int) (8::Int) (9::Int) :: Result String) -- let t3 = unResult (test (5::Int) :: Result String) -- let t4 = unResult (test "hello" "world" :: Result String) print t1 print t2 -- print t3 -- print t4
Original post: It turns out I got most of the way there. Specifically, I am able to declare a function which:
- Accepts only a prime number of arguments.
- Accepts integers at argument positions that are fibonacci numbers.
- Accepts string or integers at positions that are not fibonacci numbers.
It’s certain that there is some way to accomplish that, because the type system is, after all, Turing complete. However, I’m unable to figure it out at the moment. Perhaps someone else can step in and help.
{-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module WackyStuff where {- Obvious we'll need type-level integers, so let's build some. -} data Zero data Succ a type One = Succ Zero ------------------------------------------------------------------------------- {- To handle the more complex requirements coming up, we really need general type-level arithmetic functions. -} type family a :+: b type instance Zero :+: x = x type instance (Succ x) :+: y = Succ (x :+: y) type family a :*: b type instance Zero :*: x = Zero type instance (Succ x) :*: y = y :+: (x :*: y) -- Subtraction gives 0 if a < b type family a :-: b type instance Zero :-: a = Zero type instance (Succ a) :-: Zero = Succ a type instance (Succ a) :-: (Succ b) = a :-: b -- Division rounds all fractions up. Yeah, that's weird... but it's -- documented, so it's not a bug. :) type family a :/: b type instance Zero :/: b = Zero type instance (Succ a) :/: b = Succ (((Succ a) :-: b) :/: b) {- We now want some predicates on numbers. We're working up to primality testing here. -} class NotEqual a b instance NotEqual (Succ x) Zero instance NotEqual Zero (Succ x) instance (NotEqual x y) => NotEqual (Succ x) (Succ y) class Divis a b instance (((a :/: b) :*: b) ~ a) => Divis a b class NotDivis a b instance (NotEqual ((a :/: b) :*: b) a) => NotDivis a b {- And some divisibility checking... -} type Two = Succ One type SSucc x = Succ (Succ x) type SSSucc x = Succ (SSucc x) class NotDivisLess a b instance NotDivisLess a Two instance (NotDivis a (SSucc x), NotDivisLess a (SSucc x)) => NotDivisLess a (SSSucc x) class Prime a instance (NotDivisLess (SSucc n) (SSucc n)) => Prime (SSucc n) ------------------------------------------------------------------------------- {- Now we just need to look at fibonacci numbers. Writing a fib function is easy (if you don't care about performance anyway, which we've certainly decided not to!) -} type family Fib a type instance Fib Zero = Zero type instance Fib One = One type instance Fib (Succ (Succ x)) = (Fib x) :+: (Fib (Succ x)) {- Writing the predicate here is unusually tricky for me. Perhaps because I am missing some basic concept; but I think it's because the "or" logical connective is difficult to express in type-level programming. In any case, I can write a NotFib connective... which is unusual, but it works. Even this is ugly: I rely on the property F_n > n, which is true for n > 5, which means I need to special case lower numbers. -} type SSSSSSucc a = SSSucc (SSSucc a) type SSSSSucc a = SSucc (SSSucc a) type Four = SSucc Two type Five = Succ Four class NotFibUpTo n k -- Assumes n > 5 instance NotFibUpTo n Five instance (NotEqual (Fib (SSSSSSucc k)) n, NotFibUpTo n (SSSSSucc k)) => NotFibUpTo n (SSSSSSucc k) class NotFib n instance NotFib Four instance NotFibUpTo (SSSSSSucc n) (SSSSSSucc n) => NotFib (SSSSSSucc n) class IsFib n instance IsFib x -- I give up. Help! ------------------------------------------------------------------------------- {- Now for the final goal: We define 'wackyfunc', which is the function we are building. -} wackyfunc :: WackyFunction f String => f wackyfunc = wackyfold "" (flip (++)) (flip (flip (++) . show)) {- This wrapper around the result prevents some ambiguities that I think are actually problems in the spec itself. (Specifically, what happens if the result type is itself a function. If the result type is made explicit, then this could be removed.) -} newtype Result a = Result { unResult :: a } deriving Show {- We now build another type function that converts a type-level integer n to an n-ary function time, provided n is prime. This is the first type class that actually has a member. The member is just a generic fold, which we can use to implement functions of this type. -} class WackyFunction f x where wackyfold :: x -> (x -> String -> x) -> (x -> Int -> x) -> f instance (Prime (NumParams f), HasFibProp f x) => WackyFunction f x where wackyfold = fibfold {- Here is our type function to count parameters. You can clearly see how it would be ambiguous without the Result wrapper. -} type family NumParams f type instance NumParams (Result a) = Zero type instance NumParams (String -> x) = Succ (NumParams x) type instance NumParams (Int -> x) = Succ (NumParams x) {- Finally, here we have the class that actually builds the parameter list. Again, we provide a generic fold to handle it. -} class HasFibProp f x where fibfold :: x -> (x -> String -> x) -> (x -> Int -> x) -> f instance HasFibProp (Result a) a where fibfold s f g = Result s instance (HasFibProp f a, IsFib (NumParams f)) => HasFibProp (Int -> f) a where fibfold s f g n = fibfold (g s n) f g instance (HasFibProp f a, NotFib (NumParams f)) => HasFibProp (String -> f) a where fibfold s f g t = fibfold (f s t) f g
Very nice post.
The Fibonacci counting is not quite how I envisioned it. It counts parameters right to left instead of left to right and it starts counting at Zero.
Normally counting from Zero is fine, but it conflicts in my head with the prime counting. The 5 parameters are prime and I would number them 1 2 3 4 5 from left right not 4 3 2 1 0 as is done here.
I made a variant of fibfold & wacky type that works how I picture it, which the comment formatting will probably eat:
class F2 accum f r where
fibfold2 :: accum -> a -> (String -> a -> a) -> (Int -> a -> a) -> (a -> r) -> f
instance F2 accum (Result r) r where
fibfold2 _ a fs fz g = Result (g a)
instance (F2 (Succ accum) f r, IsFib accum ~ HTrue) => F2 accum (Int -> f) r where
fibfold2 accum a fs fz g z = fibfold2 accum2 (fz z a) fs fz g
where inc :: a -> Succ a
inc = undefined
accum2 = undefined `asTypeOf` (inc accum)
instance (F2 (Succ accum) f r, IsFib accum ~ HFalse) => F2 accum (String -> f) r where
fibfold2 accum a fs fz g s = fibfold2 accum2 (fs s a) fs fz g
where inc :: a -> Succ a
inc = undefined
accum2 = undefined `asTypeOf` (inc accum)
And
type WackyType2 r = (F2 One f r, Prime (NumParams f) ~ HTrue) => f