Basic research on new abstract syntax

Here is the proposal that seems to incorporate all my ideas about how this stuff should work. It also makes defining new language constructs pretty simple. I also show how language constructs can be automatically grouped using newtype. This needs more fleshing out to account for things like semantic values but overall it looks good to me. This should work really well with Huet's algorithm too. We wont need lambda substitutions anymore, well just map the variable directly to the term (which might itself be a lambda). Also check out the Arity type which lets us get the best of the Vector idea along with the benefits and simplicity of curried types.

{-#LANGUAGE GADTs, KindSignatures, DataKinds, PolyKinds, TypeOperators, ViewPatterns, PatternSynonyms, RankNTypes, FlexibleContexts #-}

module Test where

--this is specil and defined by us to combine languages
data (:||:) :: ((k -> *) -> k -> *) -> ((k -> *) -> k -> *) -> (k -> *) -> k -> * where
    Mix0 :: f0 ((f0 :||: f1) a) idx -> (f0 :||: f1) a idx
    Mix1 :: f1 ((f0 :||: f1) a) idx -> (f0 :||: f1) a idx
    Unmix :: a idx -> (f0 :||: f1) a idx

--don't use type liting here
--we want to be able to define abitrary new things
--for instance here we only implement Form and Term
--but elsewhere we want to define Sequent and Rule!
--users may want to define even more stuff! like type judgements or somthing
data Form
data Term

--this is special and defined by us (implement unification in terms of this mainly)
data Language lang t where
    Atom :: Language lang t
    (:$:) :: lang (t -> t') -> lang t -> Language lang t'
    Lam :: (lang t -> lang t') -> Language lang (t -> t')

--user specifys, typically argumentless, constructors with the proper type
--this was inspired by the way lambda prolog defines 'types' and 'kinds'
data Quants :: (* -> *) -> * -> * where
    Forall :: Quants lang ((Term -> Form) -> Form)
    Exists :: Quants lang ((Term -> Form) -> Form)

data Impls :: (* -> *) -> * -> * where
    (:->) :: Impls lang (Form -> Form -> Form)
    (:<->:) :: Impls lang (Form -> Form -> Form)

--define natural numbers for type lifting
data Nat = Zero
         | Succ Nat

--think of this as a type constraint.
--Arity arg ret N T holds only if T takes N arguments of type 'arg' and returns a 'ret'
data Arity :: * -> * -> Nat -> * -> * where
    AZero :: Arity arg ret (Succ Zero) ret
    ASucc :: Arity arg ret n ret' -> Arity arg ret (Succ n) (arg -> ret')

--so now we can define pred to be mixed into the the other languages
--notice that while the type is curried we have implemented Pred for any number of argumnets
data Pred :: (* -> *) -> * -> * where
    Pred :: String -> Arity Term Form n t -> Pred lang Form

--then you can make a language like the following (but it wont be extensiable)
type MyLang lang a = ((Language :||: Quants) :||: (Impls :||: Pred)) lang a

--to make it extensiable you have to use 'newtype'
--this allows MyNewLang to be partially applied and thus extensiable
newtype MyNewLang lang a = MyNewLang (((Language :||: Quants) :||: (Impls :||: Pred)) lang a )
    --deriving(Unifiable, ...) this will automatically implement anytype class for us

gleachkr / Carnap-Old

Basic research on new abstract syntax #1