MVL.hs

{-#LANGUAGE TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances #-}
module MVL where

import Carnap.Core.Data.Types
import Carnap.Core.Data.Classes (Schematizable(..))

--A kind annotation is needed to make sure Haskell understands the kind of `lang`

data Symbol :: (* -> *) -> * -> * where
     Symbol :: String -> Symbol lang ()

data App :: (* -> *) -> * -> * where
     App :: App lang (() -> () -> ())

instance Schematizable (Symbol lang) where
    schematize (Symbol s) = const s

instance Schematizable (App lang) where
    schematize App = \(x:y:_) -> "(" ++ x ++ "," ++ y ++ ")"

type MVLex = Symbol :|: App :|: EndLang

{-  Visually:

           MVLex
          /     \
      Symbol   App :|: EndLang
                /           \
              App          EndLang

    Fx1 and Fx2 are pattern synonyms that make it a little easier to write
    long sequences of FLeft and FRight, when drilling down into complicated
    languages.

    Fx1 x = Fx (FRight (FLeft x)) takes an inhabitant of the first leaf
    (Symbol) and lifts it into the full language.

    (the first FRight skips past an uppermost occurence of Copula :|: MVLex
    introduced by FixLang - not depicted)

    Fx2 x = Fx (FRight (FRight (FLeft x))) takes an inhabitant of the
    second leaf (App) and lifts it into the full lanugage

    It's actually turned out to be more convenient in general to use
    a different technique to eliminate the FLeft/FRight boilerplate, but
    these are helpful for quick-and-dirty experimentation.
-}

type MVL = FixLang MVLex

-- CopulaSchema tells Carnap how to put together Schematizable instances to
-- create Show instances. In the simplest cases, this is just like in the
-- paper, and the default methods for CopulaSchema work fine. Generally,
-- you start to need to override the defaults when you have
-- variable-binding operators.
instance CopulaSchema MVL

sym = Fx1 . Symbol

app = Fx2 App

{-  here's an example of how to build and expression. `:!$:` is another
    pattern synonym, abbreviating something you see a few times in the paper:
    
    x :!$: y = FLeft (x :$: y)
    
    basically this is at once applying the copula and lifting the result back into
    the full language.
-}

example :: MVL ()
example = app :!$: sym "f" :!$: sym "x"