STLC in PHOAS to de Bruijn and back

PHOAS.hs

module PHOAS where

import Data.Bifunctor
import Data.Functor.Const
import Data.Kind
import Data.SOP.NP
import GHC.Show
import Unsafe.Coerce (unsafeCoerce)

{-------------------------------------------------------------------------------
  Preliminaries
-------------------------------------------------------------------------------}

-- | @Elem x xs@ is evidence that @x is an element of @xs@
data Elem :: [k] -> k -> Type where
  EZ ::              Elem (x ': xs) x
  ES :: Elem xs x -> Elem (y ': xs) x

index :: Elem xs x -> NP f xs -> f x
index EZ     (x :* _ ) = x
index (ES e) (_ :* xs) = index e xs

data Some f where
  Some :: f a -> Some f

{-------------------------------------------------------------------------------
  De Bruijn
-------------------------------------------------------------------------------}

-- | De Bruijn representation of the STLC
data DeBruijn :: [Type] -> Type -> Type where
  BVar :: Elem xs a -> DeBruijn xs a
  BLam :: DeBruijn (a ': xs) b -> DeBruijn xs (a -> b)
  BApp :: DeBruijn xs (a -> b) -> DeBruijn xs a -> DeBruijn xs b

-- | Example: @\f. \x. f x@
bExample :: DeBruijn '[] ((a -> b) -> a -> b)
bExample = BLam $ BLam $ BApp (BVar (ES EZ)) (BVar EZ)

deriving instance Show (Elem x xs)
deriving instance Show (DeBruijn xs a)

-- >>> bExample
-- BLam (BLam (BApp (BVar (ES EZ)) (BVar EZ)))

{-------------------------------------------------------------------------------
  PHOAS
-------------------------------------------------------------------------------}

data PHOAS :: (Type -> Type) -> Type -> Type where
  PVar :: f a -> PHOAS f a
  PLam :: (f a -> PHOAS f b) -> PHOAS f (a -> b)
  PApp :: PHOAS f (a -> b) -> PHOAS f a -> PHOAS f b

newtype ClosedTerm a = ClosedTerm (forall f. PHOAS f a)

-- | Example: @\f. \x. f x@ (same as above)
pExample :: ClosedTerm ((a -> b) -> a -> b)
pExample = ClosedTerm $ PLam $ \f -> PLam $ \x -> PApp (PVar f) (PVar x)

instance Show (PHOAS (Const String) a) where
  showsPrec = go 0
    where
      go :: Int -> Int -> PHOAS (Const String) b -> ShowS
      go free p = showParen (p > appPrec) . \case
          PVar (Const x) ->
                showString "PVar "
              . showString x
          PLam f ->
                showString "PLam (\\"
              . showString x
              . showString " -> "
              . go (free + 1) 0 (f (Const x))
              . showString ")"
            where
              x = "x" ++ show free
          PApp f e ->
               showString "PApp "
             . go free appPrec1 f
             . showString " "
             . go free appPrec1 e

instance Show (ClosedTerm a) where
  showsPrec p (ClosedTerm a) = showParen (p > appPrec) $
        showString "ClosedTerm "
      . showsPrec appPrec1 (a :: PHOAS (Const String) a)

-- >>> pExample
-- ClosedTerm (PLam (\x0 -> PLam (\x1 -> PApp (PVar x0) (PVar x1))))

{-------------------------------------------------------------------------------
  From de Bruijn to PHOAS
-------------------------------------------------------------------------------}

toPHOAS :: DeBruijn '[] a -> ClosedTerm a
toPHOAS = \t -> ClosedTerm (go Nil t)
  where
    go :: NP f xs -> DeBruijn xs a -> PHOAS f a
    go env (BVar x)   = PVar (index x env)
    go env (BLam f)   = PLam $ \x -> go (x :* env) f
    go env (BApp f e) = PApp (go env f) (go env e)

-- >>> toPHOAS bExample
-- ClosedTerm (PLam (\x0 -> PLam (\x1 -> PApp (PVar x0) (PVar x1))))

{-------------------------------------------------------------------------------
  From PHOAS to de Bruijn

  Turns out, this is officially a Hard Problem. As discussed in

  <https://lists.chalmers.se/pipermail/agda/2018/010033.html>

  it _is_ possible, but it needs quite a bit of machinery; it is easier with a
  cheat. For a proper solution, see for example

  <http://adam.chlipala.net/cpdt/html/Intensional.html>

  which gives a solution in Coq. That Agda mailing list post refers to

  <http://www.cse.chalmers.se/~abela/habil.pdf>

  (Section 2.5, "Liftable Terms"), and

  <https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda>

  as one possible way to cheat, but it is not clear to me quite how to translate
  that to our setting here. Two implementations of the cheat more closely
  related to our context are

  <https://homepages.inf.ed.ac.uk/slindley/papers/unembedding.pdf> (HOAS)
  <https://core.ac.uk/download/pdf/207770519.pdf> (PHOAS)

  My implementation below is perhaps the worst kind of cheat, but I'm not sure
  that we really can do much better. For sure it's not trivial.

  For one alternative appraoch, I came across

  <https://nicolaspouillard.fr/publis/names-for-free.pdf>

  The comparison to PHOAS (section 7.4) sounds pretty appealing, but I find
  the representation used in the paper not very nice. But I didn't study it
  extremely carefully; it might be worth another look.
-------------------------------------------------------------------------------}

weaken :: Some (Elem xs) -> Some (Elem (x ': xs))
weaken (Some e) = Some (ES e)

fromPHOAS :: ClosedTerm a -> DeBruijn '[] a
fromPHOAS = \(ClosedTerm t) -> go 0 [] t
  where
    go :: Int -> [(Int, Some (Elem xs))] -> PHOAS (Const Int) a -> DeBruijn xs a
    go _ env (PVar x) =
        -- Both the 'unsafeCoerce' and the 'error' calls are justified by the
        -- type correctness of the input ClosedTerm.
        BVar $ case lookup (getConst x) env of
                 Just (Some x') -> unsafeCoerce x'
                 Nothing -> error "impossible"
    go l env (PLam f) =
        BLam $ go (l + 1) ((l, Some EZ) : map (second weaken) env) (f (Const l))
    go l env (PApp f e) =
        BApp (go l env f) (go l env e)

-- >>> fromPHOAS pExample
-- BLam (BLam (BApp (BVar (ES EZ)) (BVar EZ)))