normalization by evaluation of simply-typed lambda calculus in Purescript

nbe.purs

import Control.Alternative (empty)
import Data.Generic.Rep (class Generic)
import Data.Map (Map)
import Data.Map as Map
import Data.Maybe (fromJust)
import Data.Show.Generic (genericShow)
import Effect (Effect)
import Effect.Class.Console as Console
import Effect.Ref as Ref
import Effect.Unsafe (unsafePerformEffect)
import Partial.Unsafe (unsafeCrashWith, unsafePartial)

data Ty
  = Un
  | Arr Ty Ty

derive instance Generic Ty _

instance Show Ty where
  show x = genericShow x

data Syn
  = It
  | Var String
  | Lam String Syn
  | App Syn Syn

derive instance Generic Syn _

instance Show Syn where
  show x = genericShow x

data Sem
  = Fun (Sem -> Sem)
  | Syn Syn

type Ctx = Map String Sem

main :: Effect Unit
main = do

  fresh_var_counter <- Ref.new 0
  let next_fresh_symbol _ = fresh_var_counter # Ref.modify (_ + 1) # map (show >>> ("#" <> _)) # unsafePerformEffect

  let
    reflect :: Partial => Ty -> Syn -> Sem
    reflect Un syn = Syn syn
    reflect (Arr alpha beta) syn =
      Fun \x -> reflect beta (App syn (reify alpha x))

    reify :: Partial => Ty -> Sem -> Syn
    reify Un (Syn syn) = syn
    reify (Arr alpha beta) (Fun f) = Lam x (reify beta (f (reflect alpha (Var x))))
      where
      x = next_fresh_symbol unit
    reify ty _ = unsafeCrashWith $ "reify " <> show ty <> " " <> "<sem>"

  let
    denote :: Partial => Ctx -> Syn -> Sem
    denote _ It = Syn It
    denote gamma (Var x) = Map.lookup x gamma # fromJust
    denote gamma (Lam x b) = Fun \f -> denote (gamma # Map.insert x f) b
    denote gamma (App f a) = case denote gamma f of
      Fun f' -> f' (denote gamma a)
      _ -> unsafeCrashWith $ "denote " <> show (gamma # Map.keys) <> " " <> show (App f a) <> " | " <> "denote " <> show (gamma # Map.keys) <> show f <> " = " <> show "<sem>"

    norm :: Partial => Ty -> Syn -> Syn
    norm alpha syn = reify alpha (denote empty syn)

  unsafePartial do
    Console.logShow $ norm Un $ App (Lam "x" (Var "x")) It

  pure unit