I thought I would share an old piece of code that I’ve had lying around for a while. Basically, it calculates Fibonacci numbers in the type system:
{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses,
FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
module Fibonacci where
data Nat
data S a = S a
class Numeral a where
value :: a -> Integer
prev :: S a -> a
prev = undefined
instance Numeral Nat where
value _ = 0
instance (Numeral a) => Numeral (S a) where
value x = 1 + (value . prev $ x)
class Add a b c | a b -> c where
add :: a -> b -> c
instance Add Nat b b where
add = undefined
instance Add a b c => Add (S a) b (S c) where
add = undefined
class Fib a b | a -> b where
fib :: a -> b
instance Fib Nat Nat where
fib = undefined
instance Fib (S Nat) (S Nat) where
fib = undefined
instance (Fib (S a) b, Fib a c, Add b c d) => Fib (S (S a)) d where
fib x = undefined
main = print . value . fib . S . S . S . S . S
. S . S . S . S $ (undefined :: Nat)
