{- $Id: tagless.hs,v 1.3 2025/01/01 00:18:53 flo Exp $ -}
{- A Tagless Interpreter in Haskell
This is based on the `TaglessDep` chapter of Adam Chlipala's CPDT, translating the Coq Formalisation as directly as possible into Haskell.
In particular, this is an exercise in using type families
-}
-- We need to enable some language extensions:
{-# LANGUAGE GADTs, StandaloneDeriving, KindSignatures, DataKinds, TypeFamilies #-}
{-
- GADTs :: Generalized Algebraic Data Types allow richer return types
  for inductive constructors. This is needed for the `Exp` type later.
- StandaloneDeriving :: A simple syntax extension allowing typeclass
  deriving for GADTs.
- DataKinds :: This promotes every data type to a kind and its
  constructors to type constructors.
- TypeFamilies :: Allows indexed type and data families.
  We only use indexed type families here.
-}

import Data.Kind

-- We declare a type of for types in our toy language
data TType = TNat | TBool | TProd TType TType

-- A type of expressions.
-- GADTs allow us to keep the "tag" on the type level
data Exp :: TType -> Type where
  NConst :: Int -> Exp TNat
  Plus   :: Exp TNat -> Exp TNat -> Exp TNat
  Eq     :: Exp TNat -> Exp TNat -> Exp TBool
  BConst :: Bool -> Exp TBool
  And    :: Exp TBool -> Exp TBool -> Exp TBool
  If     :: Exp TBool -> Exp a -> Exp a -> Exp a
  Pair   :: Exp a -> Exp b -> Exp (TProd a b)
  Fst    :: Exp (TProd a b) -> Exp a
  Snd    :: Exp (TProd a b) -> Exp b

deriving instance (Show (Exp a))

-- We declare a family of types indexed on our type constructors.
-- In Coq, this corresponds to a function into Set/Type
type family Tdenote (t :: TType) where
  Tdenote TNat = Int
  Tdenote TBool = Bool
  Tdenote (TProd a b) = (Tdenote a, Tdenote b)

-- The denotation of expressions now follows simply by pattern-matching on the input
denote :: Exp t -> Tdenote t
denote (NConst n) = n
denote (Plus a b) = denote a + denote b
denote (Eq a b) = denote a == denote b
denote (BConst b) = b
denote (And a b) = denote a && denote b
denote (If c a b) = if denote c then denote a else denote b
denote (Pair a b) = (denote a, denote b)
denote (Fst e) = fst $ denote e
denote (Snd e) = snd $ denote e

-- Here we need a type family to simulate dependent pattern matching.
type family PairOut (e :: TType) where
  PairOut (TProd a b) = (Exp a, Exp b)
  PairOut _ = ()

pairOut :: Exp t -> Maybe (PairOut t)
pairOut (Pair a b) = Just (a, b)
pairOut _ = Nothing

cfold :: Exp t -> Exp t
cfold (NConst n) = NConst n
cfold (Plus e1 e2) =
  case (cfold e1, cfold e2)  of
    (NConst n1, NConst n2) -> NConst (n1 + n2)
    (e1',e2') -> Plus e1' e2'
cfold (Eq e1 e2) =
  case (cfold e1, cfold e2)  of
    (NConst n1, NConst n2) -> BConst (n1 == n2)
    (e1',e2') -> Eq e1' e2'
cfold (BConst b) = BConst b
cfold (And e1 e2) =
  case (cfold e1, cfold e2)  of
    (BConst n1, BConst n2) -> BConst (n1 && n2)
    (e1',e2') -> And e1' e2'
cfold (If e e1 e2) =
  case cfold e of
    (BConst True) -> cfold e1
    (BConst False) -> cfold e2
    e' -> If e' (cfold e1) (cfold e2)
cfold (Pair e1 e2) = Pair (cfold e1) (cfold e2)
cfold (Fst e) =
  let e' = cfold e in
    case pairOut e' of
      (Just p) -> fst p
      Nothing -> Fst e'
cfold (Snd e) =
  let e' = cfold e in
    case pairOut e' of
      (Just p) -> snd p
      Nothing -> Snd e'