Created
September 3, 2011 03:24
-
-
Save kizzx2/1190493 to your computer and use it in GitHub Desktop.
Haskell type-level programming using functional dependencies and type families
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE OverlappingInstances #-} | |
{-# LANGUAGE TypeSynonymInstances #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
-- Type-level functions using functional dependencies | |
module DepFun where | |
data Zero | |
data Succ a | |
type One = Succ Zero | |
type Two = Succ One | |
type Three = Succ Two | |
type Four = Succ Three | |
zero = undefined :: Zero | |
one = undefined :: One | |
two = undefined :: Two | |
three = undefined :: Three | |
four = undefined :: Four | |
sixteen = mult four four | |
class Add a b c | a b -> c where | |
add :: a -> b -> c | |
add _ _ = undefined | |
instance Add Zero b b | |
instance Add One b (Succ b) | |
instance Add a b c => Add (Succ a) b (Succ c) | |
class Minus a b c | a b -> c where | |
minus :: a -> b -> c | |
minus _ _ = undefined | |
instance Minus a Zero a | |
instance Minus a b (Succ c) => Minus a (Succ b) c | |
class Val a where val :: a -> Integer | |
instance Val Zero where val = const 0 | |
instance Val a => Val (Succ a) where | |
val x = 1 + val prev | |
where prev = minus x one | |
class Mult a b c | a b -> c where | |
mult :: a -> b -> c | |
mult _ _ = undefined | |
instance Mult Zero a Zero | |
instance Mult One a a | |
instance (Mult a b d, Add b d c) => Mult (Succ a) b c | |
foo = print 16 | |
bar = print . val $ mult four four | |
main = foo >> bar |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE TypeFamilies #-} | |
data Zero | |
data Succ a | |
type One = Succ Zero | |
type Two = Succ One | |
type Three = Succ Two | |
type Four = Succ Three | |
zero = undefined :: Zero | |
one = undefined :: Succ Zero | |
two = undefined :: Succ One | |
three = undefined :: Succ Two | |
four = undefined :: Succ Three | |
sixteen = mult four four | |
type family Add a b | |
type instance Add Zero b = b | |
type instance Add (Succ a) b = Succ (Add a b) | |
type family Minus a b | |
type instance Minus a Zero = a | |
type instance Minus (Succ a) (Succ b) = Minus a b | |
type family Mult a b | |
type instance Mult Zero a = Zero | |
type instance Mult (Succ a) b = Add (Mult a b) b | |
add :: a -> b -> Add a b | |
add = undefined | |
minus :: a -> b -> Minus a b | |
minus = undefined | |
mult :: a -> b -> Mult a b | |
mult = undefined | |
class Value a where value :: a -> Integer | |
instance Value Zero where | |
value = const 0 | |
instance Value a => Value (Succ a) where | |
value x = 1 + (value (minus x one)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment