Wednesday 21 January 2009

alternative beta-eta equality test


import Prelude hiding (lookup,($))
import Control.Monad

type Ref = Integer

data V
= Neutral N
| Lam (V -> V)
| Pi V (V -> V)
| Set
| Type

data N
= App N V
| Var Ref

Neutral n $ x = Neutral (App n x)
Lam f $ x = f x

lookup ((i, tau) : gamma) j
| i == j = Just tau
| otherwise = lookup gamma j
lookup [] _ = Nothing

eq 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 t

eqT 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 = True

eqN 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

No comments: