A safe interface to HOAS by selectively hiding constructors.

SafeHOAS.hs

{-# LANGUAGE PatternSynonyms, ViewPatterns, DataKinds #-}
module SafeHoas (BuildExp, app, lam, MatchExp (Var, App, Lam), shift) where

import Data.Coerce

type Name = String

data Exp = Var' Name | App' Exp Exp | Lam' (Exp -> Exp)

newtype BuildExp (s :: ()) = BuildExp Exp

app :: BuildExp s -> BuildExp s -> BuildExp s
app = coerce App'

lam :: (BuildExp s -> BuildExp s) -> BuildExp s
lam = coerce Lam'

newtype MatchExp = MatchExp Exp

pattern Var :: Name -> MatchExp
pattern Var v <- (coerce -> Var' v)

pattern App :: MatchExp -> MatchExp -> MatchExp
pattern App x y <- (coerce -> App' (coerce -> x) (coerce -> y))

pattern Lam :: (Name -> MatchExp) -> MatchExp
pattern Lam x <- (coerce -> Lam' ((\f -> coerce . f . Var') -> x))

-- Thanks to Zhixuan Yang for the idea of using the 's' parameter for this!
shift :: (forall s. BuildExp s) -> MatchExp
shift x = coerce x