Example from Chapter 2 of CPDT in modern Haskell

stack.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}
module Main (main) where

import Numeric.Natural (Natural)

main :: IO ()
main = do
  print (expDenote (ConstNat 42))
  print (progDenote (compile (ConstNat 42) :: Result 'Nat) ())
  print (expDenote (ConstBool True))
  print (progDenote (compile (ConstBool True) :: Result 'Bool) ())
  print (expDenote (Binop Times (Binop Plus (ConstNat 2) (ConstNat 2)) (ConstNat 7)))
  print (progDenote (compile (Binop Times (Binop Plus (ConstNat 2) (ConstNat 2)) (ConstNat 7)) :: Result 'Nat) ())
  print (expDenote (Binop Eq (Binop Plus (ConstNat 2) (ConstNat 2)) (ConstNat 7)))
  print (progDenote (compile (Binop Eq (Binop Plus (ConstNat 2) (ConstNat 2)) (ConstNat 7)) :: Result 'Bool) ())
  print (expDenote (Binop Lt (Binop Plus (ConstNat 2) (ConstNat 2)) (ConstNat 7)))
  print (progDenote (compile (Binop Lt (Binop Plus (ConstNat 2) (ConstNat 2)) (ConstNat 7)) :: Result 'Bool) ())

type Nat = Natural

data Type = Nat | Bool

data Binop :: Type -> Type -> Type -> * where
  Plus :: Binop 'Nat 'Nat 'Nat
  Times :: Binop 'Nat 'Nat 'Nat
  Eq :: forall ty. Eq (TypeDenote ty) => Binop ty ty 'Bool
  Lt :: Binop 'Nat 'Nat 'Bool

data Exp :: Type -> * where
  ConstNat :: Nat -> Exp 'Nat
  ConstBool :: Bool -> Exp 'Bool
  Binop :: forall ty1 ty2 r. Binop ty1 ty2 r -> Exp ty1 -> Exp ty2 -> Exp r

type family TypeDenote (x :: Type) :: * where
  TypeDenote 'Nat = Nat
  TypeDenote 'Bool = Bool

binopDenote :: Binop ty1 ty2 r -> TypeDenote ty1 -> TypeDenote ty2 -> TypeDenote r
binopDenote = \case
  Plus -> (+)
  Times -> (*)
  Eq -> (==)
  Lt -> (<=)

expDenote :: Exp ty -> TypeDenote ty
expDenote = \case
  ConstNat n -> n
  ConstBool b -> b
  Binop op e1 e2 -> binopDenote op (expDenote e1) (expDenote e2)

-- type Stack = [Type]
--
-- data Instr :: Stack -> Stack -> * where
--     ‘Stack’ of kind ‘*’ is not promotable
--         In the kind ‘Stack -> Stack -> *’

data Instr :: [Type] -> [Type] -> * where
  InstrNat :: Nat -> Instr s ('Nat ': s)
  InstrBool :: Bool -> Instr s ('Bool ': s)
  InstrBinop :: Binop ty1 ty2 r -> Instr (ty1 ': ty2 ': s) (r ': s)

data Prog :: [Type] -> [Type] -> * where
  Nil :: Prog s s
  Cons :: Instr s1 s2 -> Prog s2 s3 -> Prog s1 s3

type Result r = Prog '[] '[r]

type (*) = (,)

type family StackDenote (tys :: [Type]) :: * where
  StackDenote '[] = ()
  StackDenote (ty ': tys) = TypeDenote ty * StackDenote tys

instrDenote :: Instr tys tys' -> StackDenote tys -> StackDenote tys'
instrDenote = \case
  InstrNat n -> \s -> (n, s)
  InstrBool b -> \s -> (b, s)
  InstrBinop op -> \s -> let
      (e1, (e2, s')) = s
    in
      (binopDenote op e1 e2, s')

progDenote :: Prog tys tys' -> StackDenote tys -> StackDenote tys'
progDenote = \case
  Nil -> \s -> s
  Cons i p' -> \s -> progDenote p' (instrDenote i s)

infixr 5 ~>
(~>) :: Prog tys tys' -> Prog tys' tys'' -> Prog tys tys''
(~>) = \case
  Nil -> \p -> p
  Cons i p -> \p' -> Cons i (p ~> p')

compile :: Exp ty -> Prog tys (ty ': tys)
compile = \case
  ConstNat n -> Cons (InstrNat n) Nil
  ConstBool b -> Cons (InstrBool b) Nil
  Binop op e1 e2 ->
    compile e2 ~> compile e1 ~> Cons (InstrBinop op) Nil