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`