Skip to content

Instantly share code, notes, and snippets.

@TerrorJack
Created June 1, 2018 07:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save TerrorJack/49c0cc3d527206e75012a1145f959e78 to your computer and use it in GitHub Desktop.
Save TerrorJack/49c0cc3d527206e75012a1145f959e78 to your computer and use it in GitHub Desktop.
{-# LANGUAGE DataKinds, GADTs #-}
import Data.Data
data Phase
= PS
| PI
data Term a where
S :: String -> Term 'PS
I :: Int -> Term 'PI
P :: Term a -> Term a -> Term a
subst :: (String -> Int) -> Term 'PS -> Term 'PI
subst = undefined
substDeep :: (Data (c 'PS), Data (c 'PI)) => (String -> Int) -> c 'PS -> c 'PI
substDeep = undefined
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment