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:

1. Accepts only a prime number of arguments.
2. Accepts integers at argument positions that are fibonacci numbers.
3. 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

About these ads