Wednesday 21 January 2009

alternative beta-eta equality test

`import Prelude hiding (lookup,(\$))import Control.Monadtype Ref = Integerdata V = Neutral N | Lam (V -> V) | Pi V (V -> V) | Set | Typedata N = App N V | Var RefNeutral n \$ x = Neutral (App n x)Lam f \$ x = f xlookup ((i, tau) : gamma) j | i == j = Just tau | otherwise = lookup gamma jlookup [] _ = Nothingeq gamma i f g (Pi tau sigmaF) = eq ((i, tau) : gamma) (i+1) (f \$ x) (g \$ x) (sigmaF x) where x = Neutral (Var i)eq gamma i (Neutral n) (Neutral m) Set = maybe False (const True) (eqN gamma i n m)eq gamma i s t Type = eqT gamma i s teqT gamma i (Pi s tF) (Pi u vF) = eqT gamma i s u && eqT ((i, s) : gamma) (i+1) (tF x) (vF x) where x = Neutral (Var i)eqT gamma i Set Set = TrueeqN gamma i (App n x) (App m y) = do Pi tau sigmaF <- eqN gamma i n m guard (eq gamma i x y tau) return (sigmaF x)eqN gamma _ (Var i) (Var j) | i == j = lookup gamma i | otherwise = Nothing-- test = eq [] 0--   (Lam (\x -> x))--   (Lam (\f -> Lam (\x -> f \$ x)))--   (Pi (Pi Set (\_ -> Set)) (\_ -> (Pi Set (\_ -> Set))))-- > test-- True`

Monday 12 January 2009

Data.Dynamic without typeclasses or unsafeCoerce

`{-# LANGUAGE RankNTypes, GADTs #-}data DYN t where BOOL :: DYN Bool INT :: DYN Integer (:->:) :: DYN a -> DYN b -> DYN (a -> b)data DYNAMIC where UnDYNAMIC :: DYN t -> t -> DYNAMICdata Equal a b where REFL :: Equal x xmkDyn :: DYN t -> t -> DYNAMICmkDyn code obj = UnDYNAMIC code objdecide :: DYN t -> DYN u -> Maybe (Equal t u)decide BOOL BOOL = Just REFLdecide INT INT = Just REFLdecide (u :->: v) (p :->: q) = do REFL <- decide u p; REFL <- decide v q; return REFLdecide _ _ = Nothingunbox :: DYNAMIC -> DYN t -> Maybe tunbox (UnDYNAMIC t e) u = do REFL <- decide t u; return elist = [ mkDyn BOOL True, mkDyn INT 34, mkDyn (BOOL :->: INT) (\x -> if x then 32 else 56) ]-- > unbox (list !! 0) BOOL-- Just True-- > unbox (list !! 1) BOOL-- Nothing-- > unbox (list !! 2) BOOL-- Nothing---- > unbox (list !! 0) INT-- Nothing-- > unbox (list !! 1) INT-- Just 34-- > unbox (list !! 2) INT-- Nothing---- > fmap (\$ True) (unbox (list !! 2) (BOOL:->:INT))-- Just 32-- > fmap (\$ False) (unbox (list !! 2) (BOOL:->:INT))-- Just 56-- > fmap (\$ True) (unbox (list !! 1) (BOOL:->:INT))-- Nothing`

Tuesday 6 January 2009

`{-# LANGUAGE GADTs #-}data CON f a fa k z where CTR :: c -> CON f a c z z VAR :: CON f a (a -> r) k z -> CON f a r (a -> k) z REC :: CON f a (f a -> r) k z -> CON f a r (f a -> k) zinfixr :+:data SUM f a ka z where ZRO :: SUM f a (f a -> z) z (:+:) :: CON f a (f a) k z -> SUM f a ka z -> SUM f a (k -> ka) zsize :: kase -> SUM f a kase Integer -> f a -> Integersize kase code = size' kase code kase codesize' :: kase -> SUM f a kase Integer -> ka -> SUM f a ka Integer -> f a -> Integersize' kase code ka ZRO = kasize' kase code ka (t :+: ts) = size' kase code (ka (sizeCON kase code 0 t)) tssizeCON :: kase -> SUM f a kase Integer -> Integer -> CON f a i0 k Integer -> ksizeCON kase code k (CTR _) = 0 + ksizeCON kase code k (VAR r) = \_ -> sizeCON kase code (1 + k) rsizeCON kase code k (REC r) = \x -> sizeCON kase code (size kase code x + k) rdfs :: kase -> SUM f a kase [a] -> f a -> [a]dfs kase code = dfs' kase code kase codedfs' :: kase -> SUM f a kase [a] -> ka -> SUM f a ka [a] -> f a -> [a]dfs' kase code ka ZRO = kadfs' kase code ka (t :+: ts) = dfs' kase code (ka (dfsCON kase code [] t)) tsdfsCON :: kase -> SUM f a kase [a] -> [a] -> CON f a i0 k [a] -> kdfsCON kase code k (CTR _) = kdfsCON kase code k (VAR r) = \a -> dfsCON kase code (a : k) rdfsCON kase code k (REC r) = \x -> dfsCON kase code (dfs kase code x ++ k) rdata Both a = a :&: a(&) = VAR (VAR (CTR (:&:)))both = (&) :+: ZRObothCase (&) (x :&: y) = x & ybothCaseR (&) (x :&: y) = y & xdata List a = Nil | Cons a (List a)nil = CTR (Nil)cons = REC (VAR (CTR (Cons)))list = nil :+: cons :+: ZROlistCase nil cons Nil = nillistCase nil cons (Cons x xs) = cons x xslistCaseR nil cons Nil = nillistCaseR nil cons (Cons x xs) = cons xs xdata Tree a = Leaf a | Branch (Tree a) (Tree a)leaf = VAR (CTR (Leaf))branch = REC (REC (CTR Branch))tree = leaf :+: branch :+: ZROtreeCase leaf branch (Leaf a) = leaf atreeCase leaf branch (Branch l r) = branch l rtreeCaseR leaf branch (Leaf a) = leaf atreeCaseR leaf branch (Branch l r) = branch r l-- > size bothCaseR both (True :&: False)-- 2-- > size listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))-- 3-- > size treeCaseR tree (Branch (Leaf ()) (Branch (Branch (Leaf ()) (Leaf ())) (Leaf ())))-- 4-- > dfs listCaseR list (Cons 'x' (Cons 'y' (Cons 'z' Nil)))-- "xyz"-- > dfs treeCaseR tree (Branch (Leaf 4) (Branch (Branch (Leaf 3) (Leaf 5)) (Leaf 7)))-- [4,3,5,7]`
`{-# LANGUAGE NoMonomorphismRestriction #-}import Prelude hiding ((\$))import Control.Monadtype Ref = Intnewtype Scope a = Scope a deriving (Eq, Show)data T = O | T :->: T deriving (Eq, Show)data S = Var Ref | Lam T (Scope S) | App S S       | Quote Ref deriving (Eq, Show)abstract i t = Scope (extract 0 t) where extract r (Var j) = Var j extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b)) extract r (App m n) = App (extract r m) (extract r n) extract r (Quote j)  | j == i = Var r  | otherwise = Quote jgamma |- Var i = Just (gamma !! i)gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return vdata V = VLam (V -> V)       | VNeutral Ndata N = NApp N V       | NQuote RefVLam f \$ x = f xVNeutral n \$ x = VNeutral (NApp n x)eval delta (Var j) = delta !! jeval delta (Lam _ (Scope b)) = VLam (\x -> eval (x:delta) b)eval delta (App m n) = eval delta m \$ eval delta n------------------- OLD-- r :: T -> V -> V-- r O e = e-- r (tau :->: sigma) f = VLam (\x -> r sigma (f \$ (r tau x)))------------------- NEWr :: T -> V -> Vr O e = er (tau :->: sigma) f = f \$ VLam (\f -> r sigma (VLam (\x -> f \$ (r tau x))))q i (VLam f) = Lam O (abstract i (q (i+1) (f (VNeutral (NQuote i)))))q i (VNeutral n) = nq i nnq i (NApp m n) = App (nq i m) (q i n)nq i (NQuote j) = Quote jnf tm = fmap (q 0 . flip r (eval [] tm)) ([] |- tm)identity = Lam (O :->: O) (Scope (Var 0))dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0))))){- OLDER{-# LANGUAGE NoMonomorphismRestriction #-}import Control.Monadtype Ref = Intnewtype Scope a = Scope a deriving (Eq, Show)data T = O | T :->: T deriving (Eq, Show)data S = Var Ref | Lam T (Scope S) | App S S       | Quote Ref deriving (Eq, Show)gamma |- Var i = Just (gamma !! i)gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return vdata V = VLam T (V -> V) | VNeutral N       | VQuote Refdata N = NVar V | NApp N V       | NQuote Reflift i (Var j) | j < i = Var j | otherwise = Var (j+1)lift i (Lam t (Scope b)) = Lam t (Scope (lift (i+1) b))lift i (App m n) = App (lift i m) (lift i n)abstract i t = Scope (extract 0 t) where extract r (Var j) = Var j extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b)) extract r (App m n) = App (extract r m) (extract r n) extract r (Quote j)  | j == i = Var r  | otherwise = Quote jeta u t = Lam u (Scope (App (lift 0 t) (Var 0)))etaReify (u :->: v) (Lam t (Scope b)) delta gamma = VLam u (\x -> etaReify v b (x:delta) (u:gamma))etaReify (u :->: v) t delta gamma = etaReify (u :->: v) (eta u t) delta gammaetaReify O t delta gamma = betaEtaReify O t delta gammabetaEtaReify _   (Var i) delta gamma = delta !! ibetaEtaReify tau (Lam t (Scope b)) delta gamma = etaReify tau (Lam t (Scope b)) delta gammabetaEtaReify tau (App m n) delta gamma = app (betaEtaReify (sigma :->: tau) m delta gamma) (etaReify sigma n delta gamma) where sigma = case gamma |- n of Nothing -> error "Type error" ; Just sigma -> sigma       app (VLam _ f) x = f x       app (VNeutral n) x = VNeutral (NApp n x)       app (VQuote j) x = VNeutral (NApp (NQuote j) x)quote i (VLam t f) = Lam t (abstract i (quote (i+1) (f (VQuote i))))quote i (VNeutral n) = nquote i nquote i (VQuote j) = Quote jnquote i (NVar v) = quote i vnquote i (NApp n v) = App (nquote i n) (quote i v)nquote i (NQuote j) = Quote jbetaEtaNF p = do t <- [] |- p return (quote 0 (etaReify t p [] []))betaEtaEqual p q = do t <- [] |- p ; t' <- [] |- q ; guard (t == t') return (quote 0 (etaReify t p [] []) == quote 0 (etaReify t q [] []))identity = Lam (O :->: O) (Scope (Var 0))dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))-- > betaEtaEqual identity dollar-- Just True-}`