GrowingTrees.hs

{-# LANGUAGE TypeFamilies, DataKinds, ConstraintKinds #-}
{-# LANGUAGE GADTs, EmptyCase, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators, PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

module Main where

-- * Void Datatype

data Void

void :: Void
void = error "Void"

absurd :: Void -> a
absurd m = case m of {}

-- * Exp Definition

data Type = Type Int

type Var = String

data Exp ex = Lit (XLit ex) Integer
            | Var (XVar ex) Var
            | Ann (XAnn ex) (Exp ex) Type
            | Abs (XAbs ex) Var (Exp ex)
            | App (XApp ex) (Exp ex) (Exp ex)

type family XLit ex
type family XVar ex
type family XAnn ex
type family XAbs ex
type family XApp ex

-- * Terminator instance

data ExpTerm
type instance XLit ExpTerm = Void
type instance XVar ExpTerm = Void
type instance XAnn ExpTerm = Void
type instance XAbs ExpTerm = Void
type instance XApp ExpTerm = Void

-- * First extension

-- Here we attach a new String field to App.

data T1 ex
type ExpT1 ex = Exp (T1 ex)
type instance XLit (T1 ex) = XLit ex
type instance XVar (T1 ex) = XVar ex
type instance XAnn (T1 ex) = XAnn ex
type instance XAbs (T1 ex) = XAbs ex
type instance XApp (T1 ex) = (String, XApp ex)

-- * Second extension (builds ontop of first)

-- Here we attach a new Int field to Ann.

data T2 ex
type ExpT2 ex = ExpT1 (T2 ex)
type instance XLit (T2 ex) = XLit ex
type instance XVar (T2 ex) = XVar ex
type instance XAnn (T2 ex) = (Int, XAnn ex)
type instance XAbs (T2 ex) = XAbs ex
type instance XApp (T2 ex) = XApp ex

-- * Using the termaintor instance

type ExpT1t = ExpT1 ExpTerm
type ExpT2t = ExpT2 ExpTerm

-- * Example instantiations

lit_T1t :: ExpT1t
lit_T1t = Lit void 42

app_T1t :: ExpT1t
app_T1t = App ("new field 1",void) lit_T1t lit_T1t

lit_T2t :: ExpT2t
lit_T2t = Lit void 42

app_T2t :: ExpT2t
app_T2t = App ("new field 1",void) lit_T2t lit_T2t

ann_T2t :: ExpT2t
ann_T2t = Ann (21,void) lit_T2t (Type 16)

-- * Dummy main

main :: IO ()
main = putStrLn "Hello World"