ReleNorm.hs

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies,
    RankNTypes, PolyKinds, FlexibleInstances, FlexibleContexts,
    MultiParamTypeClasses, StandaloneDeriving,
    ScopedTypeVariables #-}

module ReleNorm where

{-----------------------------------------------------------------------------
This file contains an implementation of relevant normalization for untyped
lambda terms.

A relevant normal form is a normal form which uses all free variables at
least once. Relevant normal forms must thus distinguish constant functions
from functions which use their argument (i.e., relevant functions), as
well as ensuring an absence of beta redexes.

Relevant normalization of an open term over an input scope
computes (partially, natch)
its relevant normal form over some output scope
and the embedding of the output scope into the input scope.
-----------------------------------------------------------------------------}


------------------------------------------------------------------------------
-- NATURAL NUMBERS
------------------------------------------------------------------------------

-- usual type level numbers and singletons
data Nat = Z | S Nat deriving Show

-- working with Nat-indexed things, we'll sometimes need to know "all Show"
class ShowN (f :: Nat -> *) where
  showN :: f n -> String


------------------------------------------------------------------------------
-- LAMBDA CALCULUS
------------------------------------------------------------------------------

-- Yer traditional well scoped lambda terms with de Bruijn indices
data Tm :: Nat -> * where
  V     :: Fin n -> Tm n            -- for Fin, see below
  (:$)  :: Tm n -> Tm n -> Tm n
  L     :: Tm (S n) -> Tm n
deriving instance Show (Tm n)
instance ShowN Tm where showN = show


------------------------------------------------------------------------------
-- ORDER PRESERVING EMBEDDINGS
------------------------------------------------------------------------------

data OPE :: Nat -> Nat -> * where
  OPEI :: OPE n n                     -- convenient redundancy
  OPES :: OPE n m -> OPE (S n) (S m)  -- OPES OPEI ~ OPEI
  OPEN :: OPE Z m                     -- OPEN Zy ~ OPEI Zy
  OPE' :: OPE n m -> OPE n (S m)      -- OPE' OPEN ~ OPEN
instance Show (OPE n m) where
  show OPEI     = "I"
  show (OPES p) = show p ++ "|"
  show OPEN     = "0"
  show (OPE' p) = show p ++ "'"
instance ShowN (OPE n) where showN = show

-- smart constructors maximizing use of OPEI and OPEN
opeS :: OPE n m -> OPE (S n) (S m)
opeS OPEI = OPEI
opeS p    = OPES p

ope' :: OPE n m -> OPE n (S m)
ope' OPEN = OPEN
ope' p    = OPE' p

-- smart eliminators for OPEs
ope2Z :: OPE n Z -> (n ~ Z => t) -> t
ope2Z OPEI t = t
ope2Z OPEN t = t

ope2S :: (OPE n' m -> t) ->
         (forall n. n' ~ S n => OPE n m -> t) ->
         OPE n' (S m) -> t
ope2S f' fS (OPES p) = fS p
ope2S f' fS  OPEI    = fS OPEI
ope2S f' fS (OPE' p) = f' p
ope2S f' fS  OPEN    = f' OPEN

opeS2 :: (forall m. m' ~ S m => OPE (S n) (S m) -> t) ->
         OPE (S n) m' -> t
opeS2 f  OPEI    = f OPEI
opeS2 f (OPES p) = f (OPES p)
opeS2 f (OPE' p) = f (OPE' p)
         
-- composition of OPEs
(<^>) :: OPE m p -> OPE n m -> OPE n p
p      <^> OPEN   = OPEN
OPEI   <^> q      = q
p      <^> OPEI   = p
OPES p <^> OPES q = opeS (p <^> q)
OPES p <^> OPE' q = ope' (p <^> q)
OPE' p <^> q      = ope' (p <^> q)
infixl 6 <^>

-- Finite sets are OPEs from one
type Fin = OPE (S Z)

fZ :: Fin (S n)
fZ = opeS OPEN

fS :: Fin n -> Fin (S n)
fS = ope'

-- value-preserving embedding
fE :: Fin n -> Fin (S n)
fE = opeS2 (ope2S (ope' . fE) (opeS . ope'))


------------------------------------------------------------------------------
-- THINNED THINGS
------------------------------------------------------------------------------

-- A thinned f is an f over only some of the variables in scope.
data Th :: (Nat -> *) -> Nat -> * where
  (:<) :: f n -> OPE n m -> Th f m
infixr 4 :<

-- We like thinned relevant things a lot, as it standardises where thinning
-- happens.

-- Of course, thinned things are functorial in the things (and in the
-- thinnings, but that's another story).
(^$) :: (forall n. f n -> g n) -> Th f n -> Th g n
h ^$ (f :< u) = h f :< u


------------------------------------------------------------------------------
-- OPE COPRODUCTS AND RELEVANT PAIRS
------------------------------------------------------------------------------

-- Encoding pairs of OPEs with the same target,
-- ensuring that the target is *covered*.

data OPE2 :: Nat -> Nat -> Nat -> * where
  OPEII :: OPE2 m m m  -- OPESS OPEII ~ OPEII   OPEII{Z} ~ OPENI{Z} ~ OPEIN{Z}
  OPENI :: OPE2 Z m m  -- OPE'S OPENI ~ OPENI
  OPEIN :: OPE2 m Z m  -- OPES' OPEIN ~ OPEIN
  OPESS :: OPE2 n n' m -> OPE2 (S n) (S n') (S m)
  OPES' :: OPE2 n n' m -> OPE2 (S n) n' (S m)
  OPE'S :: OPE2 n n' m -> OPE2 n (S n') (S m)
instance Show (OPE2 n n' m) where
  show OPEII = "II"
  show OPENI = "0I"
  show OPEIN = "I0"
  show (OPESS p) = show p ++ "^"
  show (OPES' p) = show p ++ "/"
  show (OPE'S p) = show p ++ "\\"

-- relevant pairs
data RP :: (Nat -> *) -> (Nat -> *) -> (Nat -> *) where
  RP :: f n -> OPE2 n n' m -> g n' -> RP f g m
instance (ShowN f, ShowN g) => Show (RP f g m) where
  show (RP f p g) = "(" ++ showN f ++ " <" ++ show p ++ "> " ++ showN g ++ ")"
instance (ShowN f, ShowN g) => ShowN (RP f g) where showN = show
(<&>) :: (forall n. f n -> f' n) -> (forall n. g n -> g' n) ->
         RP f g n -> RP f' g' n
(ff <&> gg) (RP f p g) = RP (ff f) p (gg g)

-- OPEII is redundant: we really need only
opeZZ :: OPE2 Z Z Z
opeZZ = OPEII -- Zy

-- smart constructors, ya da ya da
opeSS :: OPE2 n n' m -> OPE2 (S n) (S n') (S m)
opeSS OPEII = OPEII
opeSS p     = OPESS p

opeS' :: OPE2 n n' m -> OPE2 (S n) n' (S m)
opeS' OPEIN = OPEIN
opeS' p     = OPES' p

ope'S :: OPE2 n n' m -> OPE2 n (S n') (S m)
ope'S OPENI = OPENI
ope'S p     = OPE'S p

-- extract left OPE
lope :: OPE2 n n' m -> OPE n m
lope OPEII     = OPEI
lope OPEIN     = OPEI
lope OPENI     = OPEN
lope (OPESS p) = opeS (lope p)
lope (OPES' p) = opeS (lope p)
lope (OPE'S p) = ope' (lope p)

-- extract right OPE
rope :: OPE2 n n' m -> OPE n' m
rope OPEII     = OPEI
rope OPENI     = OPEI
rope OPEIN     = OPEN
rope (OPESS p) = opeS (rope p)
rope (OPE'S p) = opeS (rope p)
rope (OPES' p) = ope' (rope p)

-- construct an OPE2 by growing its left OPE
opel :: OPE n m -> OPE2 n m m
opel  OPEI    = OPEII
opel  OPEN    = OPENI
opel (OPES p) = opeSS (opel p)
opel (OPE' p) = ope'S (opel p)

-- construct an OPE2 by growing its right OPE
oper :: OPE n m -> OPE2 m n m
oper  OPEI    = OPEII
oper  OPEN    = OPEIN
oper (OPES p) = opeSS (oper p)
oper (OPE' p) = opeS' (oper p)

-- if you have two OPEs targeting m', then we can compute the
-- OPE2 which targets the union of their images, and the OPE which
-- embeds *that* in m' (representing the points hit by neither);
-- it's a kind of coproduct calculation, being the smallest thing
-- supporting both injections

data COP :: Nat -> Nat -> Nat -> * where
  COP :: OPE2 n n' m -> OPE m m' -> COP n n' m'
cop :: OPE n m' -> OPE n' m' -> COP n n' m'
cop  OPEI          q  = COP (oper q) OPEI
cop       p   OPEI    = COP (opel p) OPEI
cop  OPEN          q  = COP OPENI q
cop       p   OPEN    = COP OPEIN p
cop (OPES p) (OPES q) = case cop p q of COP pq r -> COP (opeSS pq) (opeS r)
cop (OPES p) (OPE' q) = case cop p q of COP pq r -> COP (opeS' pq) (opeS r)
cop (OPE' p) (OPES q) = case cop p q of COP pq r -> COP (ope'S pq) (opeS r)
cop (OPE' p) (OPE' q) = case cop p q of COP pq r -> COP pq         (ope' r)

-- Correspondingly, we get the following smart constructor
-- making thinned relevant pairs from thinned things.

rp :: Th f m -> Th g m -> Th (RP f g) m
rp (f :< u) (g :< v) = case cop u v of COP p w -> RP f p g :< w


------------------------------------------------------------------------------
-- RELEVANT ASSOCIAION
------------------------------------------------------------------------------

rassocLR :: RP (RP f g) h n -> RP f (RP g h) n
rassocLR (RP (RP f p g) q h) = case ope2ASSOC p q of
  OPE2ASSOC s r -> RP f r (RP g s h)

data OPE2ASSOC :: Nat -> Nat -> Nat -> Nat -> Nat -> * where
  OPE2ASSOC :: OPE2 l m lm -> OPE2 k lm klm
            -> OPE2ASSOC k l kl m klm

ope2ASSOC :: OPE2 k l kl -> OPE2 kl m klm -> OPE2ASSOC k l kl m klm
ope2ASSOC OPEII q     = OPE2ASSOC q (opel (lope q))
ope2ASSOC OPENI q     = OPE2ASSOC q OPENI
ope2ASSOC OPEIN q     = OPE2ASSOC OPENI q
ope2ASSOC p OPEII     = OPE2ASSOC (opel (rope p)) (opel (lope p))
ope2ASSOC p OPEIN     = OPE2ASSOC OPEIN p
-- ope2ASSOC p OPENI is covered
ope2ASSOC p (OPE'S q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC (ope'S r) (ope'S s)
ope2ASSOC (OPESS p) (OPES' q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC (opeS' r) (opeSS s)
ope2ASSOC (OPE'S p) (OPES' q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC (opeS' r) (ope'S s)
ope2ASSOC (OPES' p) (OPES' q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC r (opeS' s)
ope2ASSOC (OPESS p) (OPESS q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC (opeSS r) (opeSS s)
ope2ASSOC (OPE'S p) (OPESS q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC (opeSS r) (ope'S s)
ope2ASSOC (OPES' p) (OPESS q) = case ope2ASSOC p q of
  OPE2ASSOC r s -> OPE2ASSOC (ope'S r) (opeSS s)

-- managed to avoid using this, but didn't want to throw it away!


------------------------------------------------------------------------------
-- RELEVANT NORMAL FORMS
------------------------------------------------------------------------------

-- normal terms are abstractions or applications of a var to a spine
data Nm :: Nat -> * where
  NK :: Nm m      -> Nm m
  NL :: Nm (S m)  -> Nm m
  NE :: Ne m      -> Nm m
deriving instance Show (Nm n)
instance ShowN Nm where showN = show

-- neutrals are left-nested applications of variables
data Ne :: Nat -> * where
  NV :: Ne (S Z)
  NA :: RP Ne Nm m -> Ne m
deriving instance Show (Ne n)
instance ShowN Ne where showN = show

-- reassociation of OPE2s


------------------------------------------------------------------------------
-- SELECTIONS
------------------------------------------------------------------------------

-- This may seem like an obfuscated predecessor relation, but only because
-- natural numbers are so confusing. On lists, it would be the deletion
-- relation...

data Sel :: Nat -> Nat -> * where
  Zs :: Sel (S n) n
  Ss :: Sel m n -> Sel (S m) (S n)

-- ...and besides, there's info in the inhabitant

-- When a Sel and an OPE2 interact, something hits something.

data Which :: Nat -> Nat -> Nat -> * where
  Hit0 :: Sel n0' n0               -> OPE2 n0 n1' m -> Which n0' n1' m
  Hit1 ::               Sel n1' n1 -> OPE2 n0' n1 m -> Which n0' n1' m
  Hit2 :: Sel n0' n0 -> Sel n1' n1 -> OPE2 n0  n1 m -> Which n0' n1' m

which :: Sel m' m -> OPE2 n0' n1' m' -> Which n0' n1' m
which x  OPEII     = Hit2 x  x  OPEII
which x  OPEIN     = Hit0 x     OPEIN
which x  OPENI     = Hit1    x  OPENI
which Zs (OPES' p) = Hit0 Zs    p
which Zs (OPE'S p) = Hit1    Zs p
which Zs (OPESS p) = Hit2 Zs Zs p
which (Ss x) (OPESS p) = case which x p of
  Hit0 y   q -> Hit0 (Ss y)        (opeSS q)
  Hit1   z q -> Hit1        (Ss z) (opeSS q)
  Hit2 y z q -> Hit2 (Ss y) (Ss z) (opeSS q)
which (Ss x) (OPES' p) = case which x p of
  Hit0 y   q -> Hit0 (Ss y)        (opeS' q)
  Hit1   z q -> Hit1            z  (opeS' q)
  Hit2 y z q -> Hit2 (Ss y)     z  (opeS' q)
which (Ss x) (OPE'S p) = case which x p of
  Hit0 y   q -> Hit0     y         (ope'S q)
  Hit1   z q -> Hit1        (Ss z) (ope'S q)
  Hit2 y z q -> Hit2     y  (Ss z) (ope'S q)


------------------------------------------------------------------------------
-- HEREDITARY SUBSTITUTION
------------------------------------------------------------------------------

nsub :: Th (Sel m') m -> Nm m' -> Th Nm m -> Th Nm m
nsub x        (NK t)  s       = NK ^$ nsub x t s
nsub (x :< p) (NL t) (s :< u) = abst $ nsub (Ss x :< OPES p) t (s :< OPE' u)
nsub x        (NE t)  s       = hsub x t s

abst :: Th Nm (S m) -> Th Nm m
abst (t :< w) = ope2S (NK t :<) (NL t :<) w

hsub :: Th (Sel n') m -> Ne n' -> Th Nm m -> Th Nm m
hsub _        NV              s = s
hsub (x :< p) (NA (RP f q a)) s = apply $ case which x q of
  Hit0 y   r -> (hsub (y :< p <^> lope r) f s , a :< p <^> rope r)
  Hit1   z r -> (NE f :< p <^> lope r         , nsub (z :< p <^> rope r) a s)
  Hit2 y z r -> (hsub (y :< p <^> lope r) f s , nsub (z :< p <^> rope r) a s)

apply :: (Th Nm m, Th Nm m) -> Th Nm m
apply (NK t :< u, _) = t :< u
apply (NL t :< u, s) = nsub (Zs :< u) t s
apply (NE f :< u, s) = (NE . NA) ^$ rp (f :< u) s


------------------------------------------------------------------------------
-- NORMALIZATION
------------------------------------------------------------------------------

nm :: Tm n -> Th Nm n
nm (V i)    = NE NV :< i
nm (L t)    = abst (nm t)
nm (f :$ s) = apply (nm f, nm s)

instance ShowN f => Show (Th f n) where
  show (f :< w) = showN f ++ " :< " ++ show w
instance ShowN f => ShowN (Th f) where
  showN = show


------------------------------------------------------------------------------
-- THE JIGGER
------------------------------------------------------------------------------

class LE n m where
  embed :: OPE n m

instance LE Z Z where
  embed = OPEI

instance LE Z m => LE Z (S m) where
  embed = OPE' embed

instance LE n m => LE (S n) (S m) where
  embed = case (embed :: OPE n m) of
    OPEI   -> OPEI
    OPE' p -> OPE' (jig p)

jig :: OPE n m -> OPE (S n) (S m)
jig OPEI     = OPEI
jig (OPE' p) = OPE' (jig p)

la :: forall n. ((forall m. LE (S n) m => Tm m) -> Tm (S n))
   -> Tm n
la f = L (f (V (embed <^> (fZ :: Fin (S n)))))

cl :: Tm Z -> Tm Z
cl = id


------------------------------------------------------------------------------
-- AMEN
------------------------------------------------------------------------------

add :: Tm Z
add = la$ \m -> la$ \n -> la$ \f -> la$ \x -> m :$ f :$ (n :$ f :$ x)

mult :: Tm Z
mult = la$ \m -> la$ \n -> la$ \f -> m :$ (n :$ f)

expo :: Tm Z
expo = la$ \m -> la$ \n -> n :$ m

naught :: Tm Z
naught = la$ \ f -> la$ \ x -> x

one = expo :$ naught :$ naught
two = add :$ one :$ one
four = mult :$ two :$ two