pat_staged.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
module Pat where

import qualified Language.Haskell.TH as TH (Code, Q,)
import qualified Language.Haskell.TH.Syntax as TH (Lift(..))

-- Step 1: Unstaged interpreter

data Pat input f res where
  LitPat :: Int -> Pat Int res res
  VarPat :: Pat a (a -> r) r
  NilPat :: Pat [a] r r
  ConsPat :: Pat a f g -> Pat [a] g r -> Pat [a] f r

data Case input res where
  Case ::
    Pat input f r
    -> f -> Case input r

v1 :: Pat [a] (a -> [a] -> r) r
v1 = VarPat `ConsPat` VarPat

defn1 :: Case [a] (Maybe (a,[a]))
defn1 = Case v1 (\a1 a2 -> Just (a1, a2))

defn2 :: Case [a] (Maybe x)
defn2 = Case NilPat Nothing

defn3 :: Case [Int] (Maybe (Int, [Int]))
defn3 = Case (LitPat 1 `ConsPat` VarPat) (\a2 -> Just (1, a2))


match :: a -> [Case a b] -> b
match _ [] = error "no matches"
match c (Case p l : xs) =
  case pat c p l of
    Just x -> x
    Nothing -> match c xs

pat :: a -> Pat a f r -> f -> Maybe r
pat a (LitPat n) r | n == a = Just r
                   | otherwise = Nothing
pat a VarPat r = Just (r a)
pat a NilPat r = case a of
                    [] -> Just r
                    _  -> Nothing
pat a (ConsPat p1 p2) r = case a of
                            (x:xs) ->  pat xs p2 =<< pat x p1 r
                            [] -> Nothing

-- Challenge, write a staged interpreter for `Case`
-- This attempt follows the descrption in the paper:
-- Safe Pattern Generation for Multi-Stage Programming
-- https://www.cl.cam.ac.uk/~jdy22/papers/safe-pattern-generation-for-multi-stage-programming.pdf
--
-- Clue: Using this definition it is impossible to write a well-typed staged interpreter.

type Code = TH.Code TH.Q

data PatS input f res where
  LitPatS :: Int -> PatS Int res res
  VarPatS :: PatS a (Code a -> r) r
  NilPatS :: PatS [a] r r
  ConsPatS :: PatS a f g -> PatS [a] g r -> PatS [a] f r

data CaseS input res where
  CaseS ::
    PatS input f (Code r)
    -> f -> CaseS input r


v1s :: PatS [a] (Code a -> Code [a] -> r) r
v1s = VarPatS `ConsPatS` VarPatS

defn1s :: CaseS [a] (Maybe (a,[a]))
defn1s = CaseS v1s (\a1 a2 -> [|| Just ($$a1, $$a2) ||] )

defn2s :: CaseS [a] (Maybe x)
defn2s = CaseS NilPatS ([|| Nothing ||])

defn3s :: CaseS [Int] (Maybe (Int, [Int]))
defn3s = CaseS (LitPatS 1 `ConsPatS` VarPatS) (\a2 -> [|| Just (1, $$a2) ||])

-- Challenge, write a staged interpreter for `Case`

matchS :: Code a -> [CaseS a b] -> Code b
matchS _ [] = [|| error "no matches" ||]
matchS c (CaseS p l : xs) = _