Greg Buchholz wrote:
Wow. Color me impressed. A little under a week ago, I stumbledHere's a cleaned up version, I have made the function composition and stack both
onto Joy, and thought to myself that it could be translated almost
directly into Haskell (which would imply it was possible to statically
type). Well, it wasn't quite as direct as I had initially thought, but
it looks like you've done it. Are there any papers/books out there
which I could study to learn more about these (and other) tricks of the
type system wizards?
use HLists... a bit neater. Have also added "primrec" and a 5th factorial.
As for type tricks most of these should be in the HList or OOHaskell papers. The things to notice are using types as instance labels, that constraints form horn
clause compile time meta-programs (in a non-backtracking prolog style) and that multi-parameter classes with functional depandencies simulate some dependant
types.
Keean.
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-undecidable-instances #-}--Joy implemented in Haskell... extensible embedded language... module Joy where import MainGhcGeneric1 -- Building non-empty lists type HOne = HSucc HZero hOne :: HOne hOne = undefined type HTwo = HSucc HOne hTwo :: HTwo hTwo = undefined type HThree = HSucc HTwo hThree :: HThree hThree = undefined end :: HNil end = hNil instance HList s => Apply HNil s s where apply _ s = s instance (HList s,HList s',HList l,Apply a s s',Apply l s' s'') => Apply (HCons a l) s s'' where apply (HCons a l) s = apply l (apply a s :: s') instance HList s => Apply HZero s (HCons HZero s) where apply _ s = hCons hZero s instance (HNat a,HList s) => Apply (HSucc a) s (HCons (HSucc a) s) where apply a s = hCons a s data Lit a = Lit a lit :: a -> Lit a lit a = Lit a unl :: Lit a -> a unl (Lit a) = a instance Show a => Show (Lit a) where showsPrec _ (Lit a) = showChar '[' . shows a . showChar ']' instance HList s => Apply (Lit a) s (HCons a s) where apply (Lit a) s = hCons a s class (HBool b,HList s) => HIfte b t f s s' | b t f s -> s' where hIfte :: b -> t -> f -> s -> s' instance (HList s,Apply t s s') => HIfte HTrue t f s s' where hIfte _ t _ s = apply t s instance (HList s,Apply f s s') => HIfte HFalse t f s s' where hIfte _ _ f s = apply f s data Ifte ifte :: Ifte ifte = undefined instance Show Ifte where showsPrec _ _ = showString "If" instance (Apply b s r,HHead r b',HIfte b' t f s s') => Apply Ifte (f :*: t :*: b :*: s) s' where apply _ (HCons f (HCons t (HCons b s))) = hIfte (hHead (apply b s :: r) :: b') t f s data Nul nul :: Nul nul = undefined instance Show Nul where showsPrec _ _ = showString "Nul" instance HList s => Apply Nul (HCons HZero s) (HCons HTrue s) where apply _ (HCons _ s) = hCons hTrue s instance HList s => Apply Nul (HCons (HSucc n) s) (HCons HFalse s) where apply _ (HCons _ s) = hCons hFalse s data EQ eq :: EQ eq = undefined instance Show EQ where showsPrec _ _ = showString "Eq" instance (HList s,TypeEq a b t) => Apply EQ (HCons a (HCons b s)) (HCons t s) where apply _ (HCons a (HCons b s)) = hCons (typeEq a b) s data Dip dip :: Dip dip = undefined instance Show Dip where showsPrec _ _ = showString "Dip" instance (HList s,HList s',Apply a s s') => Apply Dip (HCons a (HCons b s)) (HCons b s') where apply _ (HCons a (HCons b s)) = hCons b (apply a s) data Dup dup :: Dup dup = undefined instance Show Dup where showsPrec _ _ = showString "Dup" instance HList s => Apply Dup (HCons a s) (HCons a (HCons a s)) where apply _ s@(HCons a _) = hCons a s data Pop pop :: Pop pop = undefined instance Show Pop where showsPrec _ _ = showString "Pop" instance HList s => Apply Pop (HCons a s) s where apply _ (HCons _ s) = s data Swap swap :: Swap swap = undefined instance Show Swap where showsPrec _ _ = showString "Swap" instance HList s => Apply Swap (HCons a (HCons b s)) (HCons b (HCons a s)) where apply _ (HCons a (HCons b s)) = hCons b (hCons a s) data Suc suc :: Suc suc = undefined instance Show Suc where showsPrec _ _ = showString "Suc" instance (HNat a,HList s) => Apply Suc (HCons a s) (HCons (HSucc a) s) where apply _ (HCons _ s) = hCons (undefined::HSucc a) s data Pre pre :: Pre pre = undefined instance Show Pre where showsPrec _ _ = showString "Pre" instance (HNat a,HList s) => Apply Pre (HCons (HSucc a) s) (HCons a s) where apply _ (HCons _ s) = hCons (undefined::a) s data Add add :: Add add = undefined instance Show Add where showsPrec _ _ = showString "Add" instance (HList s,HAdd a b c) => Apply Add (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = hCons (hAdd (undefined::a) (undefined::b)) s class (HNat a,HNat b) => HAdd a b c | a b -> c where hAdd :: a -> b -> c instance HAdd HZero HZero HZero where hAdd _ _ = hZero instance HNat b => HAdd HZero (HSucc b) (HSucc b) where hAdd _ b = b instance HNat a => HAdd (HSucc a) HZero (HSucc a) where hAdd a _ = a instance (HNat (HSucc a),HNat (HSucc b),HNat c,HAdd a b c) => HAdd (HSucc a) (HSucc b) (HSucc (HSucc c)) where hAdd _ _ = hSucc $ hSucc $ hAdd (undefined::a) (undefined::b) data Sub sub :: Sub sub = undefined instance Show Sub where showsPrec _ _ = showString "Sub" instance (HList s,HSub a b c) => Apply Sub (HCons b (HCons a s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = hCons (hSub (undefined::a) (undefined::b)) s class (HNat a,HNat b) => HSub a b c | a b -> c where hSub :: a -> b -> c instance HSub HZero HZero HZero where hSub _ _ = hZero instance HNat a => HSub (HSucc a) HZero (HSucc a) where hSub a _ = a instance HNat a => HSub HZero (HSucc a) HZero where hSub _ _ = hZero instance (HSub a b c) => HSub (HSucc a) (HSucc b) c where hSub _ _ = hSub (undefined::a) (undefined::b) data Mult mult :: Mult mult = undefined instance Show Mult where showsPrec _ _ = showString "Mult" instance (HList s,HMult a b c) => Apply Mult (HCons a (HCons b s)) (HCons c s) where apply _ (HCons _ (HCons _ s)) = hCons (hMult (undefined::a) (undefined::b)) s class (HNat a,HNat b) => HMult a b c | a b -> c where hMult :: a -> b -> c instance HNat b => HMult HZero b HZero where hMult _ _ = hZero instance (HMult a b s,HAdd b s s') => HMult (HSucc a) b s' where hMult _ _ = hAdd (undefined::b) (hMult (undefined::a) (undefined::b) :: s) square = dup .*. mult .*. hNil cube = mult .*. mult .*. dup .*. dup .*. hNil data I i :: I i = undefined instance Show I where showsPrec _ _ = showString "I" instance Apply I HNil HNil where apply _ _ = hNil instance (HList s,Apply a s s') => Apply I (HCons a s) s' where apply _ (HCons a s) = apply a s data Primrec = Primrec deriving Show primrec :: Primrec primrec = undefined instance Apply z s s' => Apply Primrec (HCons nz (HCons z (HCons HZero s))) s' where apply _ (HCons _ (HCons z (HCons _ s))) = apply z s instance (HList s,Apply Primrec (HCons nz (HCons z (HCons n (HCons (HSucc n) s)))) s',Apply nz s' s'') => Apply Primrec (HCons nz (HCons z (HCons (HSucc n) s))) s'' where apply _ (HCons nz (HCons z s@(HCons _ _))) = apply nz (apply Primrec (hCons nz (hCons z (hCons (undefined::n) s)))) data Times times :: Times times = undefined instance Show Times where showsPrec _ _ = showString "Times" instance HList s => Apply Times (HCons p (HCons HZero s)) s where apply _ (HCons _ (HCons _ s)) = s instance (HNat n,HList s,HList s',Apply p s s',Apply Times (HCons p (HCons n s')) s'') => Apply Times (HCons p (HCons (HSucc n) s)) s'' where apply _ (HCons p (HCons _ s)) = apply times (hCons p (hCons (undefined::n) (apply p s))) class (HBool f,HList s) => HGenrec f r1 r2 b t s s'' | f r1 r2 b t s -> s'' where hGenrec :: f -> r1 -> r2 -> b -> t -> s -> s'' instance (HList s,Apply t s s') => HGenrec HTrue r1 r2 b t s s' where hGenrec _ _ _ _ t s = apply t s instance (HList s,HList s',Apply r1 s s', Apply (HCons (Lit (HCons (Lit b) (HCons (Lit t) (HCons (Lit r1) (HCons (Lit r2) (HCons Genrec HNil)))))) (HCons r2 HNil)) s' s'') => HGenrec HFalse r1 r2 b t s s'' where hGenrec _ r1 r2 b t s = apply (hCons (lit (hCons (lit b) (hCons (lit t) (hCons (lit r1) (hCons (lit r2) (hCons genrec hNil)))))) (hCons r2 hNil)) (apply r1 s :: s') data Genrec genrec :: Genrec genrec = undefined instance Show Genrec where showsPrec _ _ = showString "Genrec" instance (Apply b s s',HHead s' b',HGenrec b' r1 r2 b t s s'') => Apply Genrec (HCons r2 (HCons r1 (HCons t (HCons b s)))) s'' where apply _ (HCons r2 (HCons r1 (HCons t (HCons b s)))) = hGenrec (hHead (apply b s :: s') :: b') r1 r2 b t s class (HBool f,HList s) => HLinrec f b t r1 r2 s s' | f b t r1 r2 s -> s' where hLinrec :: f -> b -> t -> r1 -> r2 -> s -> s' instance (HList s,Apply t s s') => HLinrec HTrue b t r1 r2 s s' where hLinrec _ _ t _ _ s = apply t s instance (HList s,HList s',Apply r1 s s', Apply Linrec (HCons r2 (HCons r1 (HCons t (HCons b s')))) s'',Apply r2 s'' s''') => HLinrec HFalse b t r1 r2 s s''' where hLinrec _ b t r1 r2 s = apply r2 (apply linrec (hCons r2 (hCons r1 (hCons t (hCons b (apply r1 s :: s'))))) :: s'') data Linrec linrec :: Linrec linrec = undefined instance Show Linrec where showsPrec _ _ = showString "Linrec" instance (Apply b s s',HHead s' b',HLinrec b' b t r1 r2 s s'') => Apply Linrec (HCons r2 (HCons r1 (HCons t (HCons b s)))) s'' where apply _ (HCons r2 (HCons r1 (HCons t (HCons b s)))) = hLinrec (hHead (apply b s :: s') :: b') b t r1 r2 s data Fact fact :: Fact fact = undefined instance Show Fact where showsPrec _ _ = showString "Fact" instance (HList s,Apply (HCons (Lit (HCons (Lit HZero) (HCons EQ HNil))) (HCons (Lit (HCons Pop (HCons (Lit HOne) HNil))) (HCons (Lit (HCons Dup (HCons (Lit HOne) (HCons Sub (HCons Fact (HCons Mult HNil)))))) (HCons Ifte HNil)))) s s') => Apply Fact s s' where apply _ s = apply fac1 s fac1 = hCons (lit (hCons (lit hZero) (hCons eq hNil))) (hCons (lit (hCons pop (hCons (lit hOne) hNil))) (hCons (lit (hCons dup (hCons (lit hOne) (hCons sub (hCons fact (hCons mult hNil)))))) (hCons ifte hNil))) fac2 = lit (hOne .*. hOne .*. end) .*. dip .*. lit (dup .*. lit mult .*. dip .*. suc .*. end) .*. times .*. pop .*. end fac3 = lit nul .*. lit suc .*. lit (dup .*. pre .*. end) .*. lit (i .*. mult .*. end) .*. genrec .*. end fac4 = lit nul .*. lit suc .*. lit (dup .*. pre .*. end) .*. lit mult .*. linrec .*. end fac5 = lit hOne .*. lit mult .*. primrec .*. end main :: IO () main = do putStrLn $ show $ apply (lit hThree .*. fac1 .*. end) end putStrLn $ show $ apply i (fac2 .*. hThree .*. end) putStrLn $ show $ apply i (fac3 .*. hThree .*. end) putStrLn $ show $ apply i (fac4 .*. hThree .*. end) putStrLn $ show $ apply i (fac5 .*. hThree .*. end)
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
