stlc terms

Stream: Type theory

[Patrick Thomas]

Is this correct (in Haskell)? Are the types for the var term and the bound variable in the abs term the same or should they differ?

data Nat = O | S Nat
  deriving (Eq, Show)

data Type = Atomic | Arrow Type Type
  deriving (Eq, Show)

data Term = Var Nat | App Term Term | Abs Nat Type Term
  deriving (Eq, Show)


type Expr = (Term, Type)

type Context = [Expr]

type Proof = (Context, Expr)


-- Typing rules

applyVar :: Context -> Expr -> Proof
applyVar c e = if elem e c then (c, e) else error "bad input"

applyApp :: Proof -> Proof -> Proof
applyApp (c1, (t1, Arrow s11 s12)) (c2, (t2, s2)) =
  if c1 == c2 && s11 == s2 then (c1, (App t1 t2, s12)) else error "bad input"
applyApp _ _ = error "bad input"

applyAbs :: Proof -> Proof
applyAbs (((Var v, s1) : es), (t, s2)) = (es, (Abs v s1 t, Arrow s1 s2))
applyAbs _ = error "bad input"

{-
Example:

*Main> applyApp (applyVar [(Var O, Arrow Atomic Atomic), (Var (S O), Atomic)] (Var O, (Arrow Atomic Atomic))) (applyVar [(Var O, Arrow Atomic Atomic), (Var (S O), Atomic)] (Var (S O), Atomic))
([(Var O,Arrow Atomic Atomic),(Var (S O),Atomic)],(App (Var O) (Var (S O)),Atomic))
-}

[Mario Carneiro]

I think you want applyVar and similar definitions to return the type of the expression, rather than returning a context

[Mario Carneiro]

the context should be an additional argument to all the functions like a reader monad

[Mario Carneiro]

Your typing rules allow a single variable to have multiple types, which is not correct, or at least will significantly complicate substitution

[Patrick Thomas]

Are you thinking in terms of how to make it get the type of a given expression in a given context?

[Mario Carneiro]

yes, typecheckers usually have two functions, mutually defined: give me the type of a term, or check that this term has this type. The signatures are something like Context -> Term -> option Type and Context -> Term -> Type -> bool

[Mario Carneiro]

the second one is easily defined in terms of the first:

infer :: Context -> Term -> Maybe Type
...

check :: Context -> Term -> Type -> Bool
check c e ty = case infer c e of
  Just t -> t = ty
  Nothing -> False

[Mario Carneiro]

If you use error for error handling, then these can have type Type and Unit respectively, although that might cause haskell to delete calls to the unit function

[Patrick Thomas]

I see. I wasn't going for a type checker, but that was going to be the next attempt. Thank you. Do I have the data definitions right, especially in regard to the types for the var term and the bound variable in the abs term? Are the var terms just identifiers that can be added to the context and used as bound variables in abstraction?

[Mario Carneiro]

There are two general approaches here, known as "named variables" vs "de bruijn variables". You are using the "named variables" approach, even though the names are numbers here (they could be strings as well). The named variables approach has the advantage that you don't need to define or think about "lifting" terms when they go under a binder, but you do have to check for bound variable capture. de Bruijn variables refer to a binder by the number of nested binders, which makes alpha renaming and substitution a bit easier but adds lifting, and also makes it harder to read the resulting terms because the names of variables are implicit

[Mario Carneiro]

If you were to use the de bruijn variables approach, Abs would look like Abs Type Term, with no Nat argument since it always introduces the variable now named 0 and everything else shifts up

[Patrick Thomas]

I see. So the Term and Type data definitions are right for the named variables approach? I think Coq and Lean use de bruijn variables?

[Mario Carneiro]

Yes. Lean uses a combination of named and de bruijn variables called "locally nameless": variables inside a term are de bruijn, but binders are "opened" when they enter the local context, at which point they are replaced with "local constants" that are basically named variables

[Mario Carneiro]

HOL Light implements STLC using the named variables approach

[Patrick Thomas]

Interesting. Thank you!

[Patrick Thomas]

Is there a base type built into the STLC for Coq and Lean, or do inductive types take the place of that?

[Mario Carneiro]

Base types are only needed when there are no type constructors other than things like arrow. Practical systems will usually have some specific types there. Lean has a bunch of "base types": Type u and Prop, inductive types, and axiomatic constants

[Mario Carneiro]

HOL Light has bool (aka Prop) and ind (an infinite type used to build nat) as base types

[Patrick Thomas]

And types also become included as terms as an extension to the STLC?

[Mario Carneiro]

In dependently typed languages, types are also terms, so lambda and variables also appear as types

[Mario Carneiro]

well, even plain STLC often has type variables, but they are a separate class from regular variables. That's probably closer to HOL though

[Patrick Thomas]

It's not like adding another constructor like data Term = Var Nat | App Term Term | Abs Nat Type Term | TypeC Type?

[Mario Carneiro]

No, in DTT you have one inductive type containing all of the constructors of Type and Term

[Mario Carneiro]

that has the side effect of making Abs a type constructor and Arrow a term constructor, because the two syntactic classes are unified

[Mario Carneiro]

If you have an embedding like TypeC that only means that every type is a term, but doesn't permit using App and Abs in types

[Mario Carneiro]

for example list A is a type in lean which can be rendered App (Const "List") (Var 0), where App is the same App as used on terms

[Patrick Thomas]

You couldn't use App (TypeC (Const "List")) ((TypeC (Var 0))?
Would unifying them like that imply that every term is a type? That isn't true right?

[Mario Carneiro]

That would be a Term, but not a Type

[Mario Carneiro]

we want List A to be a type

[Patrick Thomas]

I see. But does unifying them in one inductive type remove the distinction between terms and types altogether? Aren't there base terms that are not types?

[Patrick Thomas]

I thought all types were terms, but not all terms were types.

[Patrick Thomas]

Is this right? Do I need to worry about the fact that inserting a value into the context that already has the value does not give an error, but overwrites the existing type for it?

-- Modified from https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html

import Data.Map


data Type = Atomic | Arrow Type Type
  deriving (Eq, Show)

data Term = Var String | App Term Term | Abs String Type Term
  deriving (Eq, Show)


type Context = Data.Map.Map String Type


getType :: Context -> Term -> Maybe Type
getType gamma (Var v) = Data.Map.lookup v gamma
getType gamma (App tm1 tm2) = do
  ty1 <- getType gamma tm1
  ty2 <- getType gamma tm2
  case ty1 of
    Arrow ty11 ty12 -> if ty11 == ty2 then return ty12 else Nothing
    _ -> Nothing
getType gamma (Abs v ty1 tm1) =
  let gamma' = Data.Map.insert v ty1 gamma in do
    ty2 <- getType gamma' tm1
    return (Arrow ty1 ty2)


{-
Examples:

*Main> getType (Data.Map.fromList [("a", Atomic)]) (Var "a")
Just Atomic

*Main> getType (Data.Map.fromList [("a", Atomic), ("b", (Arrow Atomic Atomic))]) (App (Var "b") (Var "a"))
Just Atomic

*Main> getType (Data.Map.fromList [("b", Atomic)]) (Abs "a" Atomic (Var "b"))
Just (Arrow Atomic Atomic)
-}

[Patrick Thomas]

I can't prove anything with this in its current form, correct? Not even limited propositional logic? What is the next minimal extension required to do that?

[Mario Carneiro]

Patrick Thomas said:

I see. But does unifying them in one inductive type remove the distinction between terms and types altogether? Aren't there base terms that are not types?

In DTT, the distinction between types and terms is a matter of typechecking, not syntax. A type is something whose type is * (in a haskell like language) or Sort u for lean

[Patrick Thomas]

I see.

[Mario Carneiro]

Is this right? Do I need to worry about the fact that inserting a value into the context that already has the value does not give an error, but overwrites the existing type for it?

That's okay as long as the updates to the context are functional / temporary within a scope. Once you are out of the scope with the shadowed variable the variable needs to go back to its old type

[Mario Carneiro]

you can also accomplish this by keeping the context as an ordered list and doing linear search when looking variables up in the context

[Mario Carneiro]

In haskell the former approach is easier since Data.Map is already a persistent map, and that's what you did

[Mario Carneiro]

your typechecker looks correct

[Mario Carneiro]

Patrick Thomas said:

I can't prove anything with this in its current form, correct? Not even limited propositional logic? What is the next minimal extension required to do that?

Well it's haskell, so no

[Mario Carneiro]

You can just transpose all of this to lean though

[Patrick Thomas]

You mean no type checker I write in Haskell can prove propositional logic? Because Haskell itself can't prove propositional logic?

[Mario Carneiro]

I mean if you want to prove the correctness of the typechecker

[Mario Carneiro]

If you want to write a prover in haskell that works fine

[Patrick Thomas]

Oh. No, I'm not worried about formally checking it. This is more a learning exercise for now.

[Mario Carneiro]

If you want to extend STLC to intuitionistic logic you need some more constructors like and / or

[Patrick Thomas]

Do I need to make the types act as terms first?

[Patrick Thomas]

First meaning as a requirement for proving anything.

[Mario Carneiro]

no need, if you are doing curry howard then proofs are the terms and propositions are the types

[Mario Carneiro]

you only need DTT if you want theorems about lambda terms

[Mario Carneiro]

basic propositional logic doesn't have any of that

[Patrick Thomas]

Right now the types are just things like Atomic -> (Atomic -> Atomic) right?. I haven't been able to see how that maps to something like P -> (Q -> P).

[Mario Carneiro]

You add type variables, Type = ... | TVar String

[Mario Carneiro]

then you will have a type like Arrow (TVar "P") (Arrow (TVar "Q") (TVar "P"))

[Mario Carneiro]

You don't strictly need them, you can have a function which proves P -> Q -> P for any types P and Q (which are themselves concrete types)

[Mario Carneiro]

like this:

mkK :: Type -> Type -> Term
mkK P Q = Abs "x" P (Abs "y" Q (Var "x"))

it is then a meta-theorem that getType (mkK P Q) = Just (Arrow P (Arrow Q P))

[Mario Carneiro]

but if you have type variables then you can actually verify this with P = TVar "P" and Q = TVar "Q"

[Patrick Thomas]

Oh. I was going to ask if you assign P to Atomic and Q to Atomic -> Atomic and prove Atomic -> ((Atomic -> Atomic) -> Atomic).

[Mario Carneiro]

If you transposed this all to lean, the theorem getType (mkK P Q) = Just (Arrow P (Arrow Q P)) would actually be provable

[Mario Carneiro]

but you can quickcheck it in haskell too

[Patrick Thomas]

Hmm. I might have to think on that some. So the type variable constructor replaces the Atomic constructor I have now?

[Patrick Thomas]

data Type = TVar String | Arrow Type Type
  deriving (Eq, Show)

[Mario Carneiro]

Well, you probably want one anyway since otherwise you don't have any closed terms

[Mario Carneiro]

but you can still run programs on types containing type variables so that might be sufficient for you

[Mario Carneiro]

I think the HOL type system contains arrow, constants and variables

[Patrick Thomas]

Do you mean

data Type = Atomic | Arrow Type Type | TVar String
  deriving (Eq, Show)

[Mario Carneiro]

yeah

[Patrick Thomas]

And a closed term is one with Atomic as a type?

[Mario Carneiro]

you want to distinguish the constants from the variables because there is an operation "instantiation" that substitutes all the type variables in a type or term

[Mario Carneiro]

a closed term type is one built from only Arrow and Atomic, no TVar

[Patrick Thomas]

Did you mean closed type above?

[Patrick Thomas]

Further above.

[Patrick Thomas]

Well, you probably want one anyway since otherwise you don't have any closed terms

[Mario Carneiro]

yes

[Mario Carneiro]

closed term/type means no free variables

[Mario Carneiro]

for types, since there are no variable binders, that just means no variables

[Patrick Thomas]

Oh, so if I changed the name from Atomic to Prop, this might be clearer.

[Patrick Thomas]

Is that right?

[Patrick Thomas]

No wait, how do you construct something like P : Prop in this?

[Patrick Thomas]

I guess you don't. The data construct data Type would be considered Prop?

[Patrick Thomas]

In the meta logic.

[Mario Carneiro]

yes

[Mario Carneiro]

You might want to change Atomic to True and add False though

[Patrick Thomas]

Why?

[Patrick Thomas]

Oh, because these are the possible values of propositions?

[Patrick Thomas]

I guess I'm not certain what Atomic and TVar String actually represent. If TVar String is a type variable, what is the domain of the variable? Is it instances of data Type?

[Mario Carneiro]

It is a variable which represents an arbitrary proposition/type

[Mario Carneiro]

type substitution would take a map subst : String -> Type and replace TVar P with subst P everywhere in a type/term

[Mario Carneiro]

however, it only "represents" an arbitrary type, it doesn't have to literally be something in data Type, in the same way that when you have a variable x : real in lean it represents an arbitrary real number even though only countably many of them can possibly have closed terms describing them

[Mario Carneiro]

the determination of what type variables actually range over is a meta-theoretic question and depends on the model

[Patrick Thomas]

I think I see. So why change Atomic to True and False?

[Mario Carneiro]

since you are doing propositional logic, you probably want true and false, and they serve as base types so you don't need Atomic anymore

[Mario Carneiro]

plus what would the meaning of Atomic be as a proposition?

[Patrick Thomas]

So True and False represent the possible values of propositions.

[Mario Carneiro]

they are two specific propositions; True will have a term trivial : True in it

[Patrick Thomas]

Does that mean I need to add additional term constructors?

[Mario Carneiro]

yes

[Mario Carneiro]

False will have an eliminator exfalso : Type -> Term such that exfalso T has type False -> T

[Mario Carneiro]

each type has an introduction and elimination rule

[Mario Carneiro]

and those are term constructors

[Mario Carneiro]

you should check out src#tactic.itauto.prop, which does this kind of thing for intuitionistic propositional logic

[Mario Carneiro]

prop is what you call Type and src#tactic.itauto.proof is what you call Term

[Mario Carneiro]

although it is slightly optimized for a particular kind of proof search

[Patrick Thomas]

Wait, I can't currently have types of the form Type -> Term can I?

[Mario Carneiro]

that is to say, data Term = ... | Exfalso Type

[Mario Carneiro]

and later getType _ (Exfalso t) = Just (Arrow False t)

[Patrick Thomas]

Hmm. Ok. I think.

[Notification Bot]

This topic was moved here from #new members > stlc terms by Mario Carneiro

[Mario Carneiro]

and getType _ trivial = Just True?

yes

[Patrick Thomas]

Cool. Thank you!

[Patrick Thomas]

Cool! If I did it right :)

-- Modified from https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html

import Data.Map


-- Proposition
data Type = TypeVar String -- P, Q, etc.
          | TypeTrue
          | TypeFalse
          | TypeArrow Type Type -- Implies
            deriving (Eq, Show)

-- Proof
data Term = TermVar String -- Hypothesis
          | TermTriv
          | TermExFalso Type
          | TermApp Term Term -- Implication Elimination
          | TermAbs String Type Term -- Implication Introduction
            deriving (Eq, Show)


type Context = Data.Map.Map String Type


getType :: Context -> Term -> Maybe Type
getType gamma (TermVar v) = Data.Map.lookup v gamma
getType _     TermTriv = return TypeTrue
getType _     (TermExFalso ty) = return (TypeArrow TypeFalse ty)
getType gamma (TermApp tm1 tm2) = do
  ty1 <- getType gamma tm1
  ty2 <- getType gamma tm2
  case ty1 of
    TypeArrow ty11 ty12 -> if ty11 == ty2 then return ty12 else Nothing
    _ -> Nothing
getType gamma (TermAbs v ty1 tm1) =
  let gamma' = Data.Map.insert v ty1 gamma in do
    ty2 <- getType gamma' tm1
    return (TypeArrow ty1 ty2)


{-
Examples:

*Main> getType (Data.Map.fromList []) (TermAbs "HP" (TypeVar "P") (TermAbs "HQ" (TypeVar "Q") (TermVar "HP")))
Just (TypeArrow (TypeVar "P") (TypeArrow (TypeVar "Q") (TypeVar "P")))

-}

[Patrick Thomas]

This helps clarify so much!

[Patrick Thomas]

What would be the next smallest extension? First order predicate logic?

[Mario Carneiro]

Well the code above doesn't yet have all the connectives of propositional logic

[Patrick Thomas]

That is true. I figured and and or should be straightforward to add.

[Mario Carneiro]

you could add negation, conjunction and disjunction, along with the corresponding proof terms and.mk, and.left, and.right and or.inl or.inr and or.elim

[Mario Carneiro]

you have some choices about how to present the operations: should they have type arguments or not?

[Patrick Thomas]

So, if abstraction didn't have an explicit type for the variable then you couldn't write a type checker right?

[Mario Carneiro]

Lean's and.left has type arguments, i.e. and.left P Q h is a proof of P if h is a proof of P /\ Q, but it should be clear that this isn't required for typechecking, and a lot of languages with a pairing operator leave off the types in this operator

[Mario Carneiro]

you can write a typechecker for a surprisingly sparsely typed term

[Mario Carneiro]

curry style typing is where you don't provide any types and it's still possible to typecheck those terms

[Mario Carneiro]

but assuming you don't want to do unification and infer types, you generally need type annotations whenever a variable is discharged from the context, i.e. in binders like Abs

[Mario Carneiro]

as well as when a type variable is not determined from the arguments, like or.inl and exfalso

[Patrick Thomas]

How would you type check something like lam x -> x without a type for x?

[Mario Carneiro]

You would use a metavariable: it has type ?A -> ?A

[Mario Carneiro]

a type checker can work that out without any assistance

[Patrick Thomas]

Oh! That is what those are! Ha!

[Mario Carneiro]

working with metavariables gets complicated though because you might discover additional facts about the type by its use later. For example lam x -> (x.1, x.2) has the type ?A /\ ?B -> ?A /\ ?B

[Patrick Thomas]

Ok, I'll see if I can add those, without unification and inferring types.

[Patrick Thomas]

How is this? I wasn't sure if I should use negation intro and elim instead.

-- Modified from https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html

import Data.Map


-- Proposition
data Type = TypeVar String -- P, Q, etc.
          | TypeTrue
          | TypeFalse
          | TypeImp Type Type
          | TypeAnd Type Type
          | TypeOr Type Type
          | TypeNeg Type
            deriving (Eq, Show)

-- Proof
data Term = TermVar String -- Hypothesis
          | TermTriv
          | TermExFalso Type
          | TermImpIntro String Type Term -- Abstraction
          | TermImpElim Term Term -- Application
          | TermAndIntro Term Term
          | TermAndElimLeft Term
          | TermAndElimRight Term
          | TermOrIntroLeft Term Type
          | TermOrIntroRight Type Term
          | TermOrElim Term Term Term
          | TermNeg Term
            deriving (Eq, Show)


type Context = Data.Map.Map String Type


getType :: Context -> Term -> Maybe Type
getType gamma (TermVar v) = Data.Map.lookup v gamma
getType _     TermTriv = return TypeTrue
getType _     (TermExFalso ty) = return (TypeImp TypeFalse ty)
getType gamma (TermImpIntro v tyv tm1) =
  let gamma' = Data.Map.insert v tyv gamma in do
    ty1 <- getType gamma' tm1
    return (TypeImp tyv ty1)
getType gamma (TermImpElim tm1 tm2) = do
  ty1 <- getType gamma tm1
  ty2 <- getType gamma tm2
  case ty1 of
    TypeImp ty11 ty12 -> if ty11 == ty2 then return ty12 else Nothing
    _ -> Nothing
getType gamma (TermAndIntro tm1 tm2) = do
  ty1 <- getType gamma tm1
  ty2 <- getType gamma tm2
  return (TypeAnd ty1 ty2)
getType gamma (TermAndElimLeft tm1) = do
  ty1 <- getType gamma tm1
  case ty1 of
    TypeAnd ty11 _ -> return ty11
    _ -> Nothing
getType gamma (TermAndElimRight tm1) = do
  ty1 <- getType gamma tm1
  case ty1 of
    TypeAnd _ ty12 -> return ty12
    _ -> Nothing
getType gamma (TermOrIntroLeft tm1 ty2) = do
  ty1 <- getType gamma tm1
  return (TypeOr ty1 ty2)
getType gamma (TermOrIntroRight ty1 tm2) = do
  ty2 <- getType gamma tm2
  return (TypeOr ty1 ty2)
getType gamma (TermOrElim tm1 tm2 tm3) = do
  ty1 <- getType gamma tm1
  ty2 <- getType gamma tm2
  ty3 <- getType gamma tm3
  case ty1 of
    TypeOr ty11 ty12 ->
      case ty2 of
        TypeImp ty21 ty22 ->
          case ty3 of
            TypeImp ty31 ty32 ->
              if ty21 == ty11 &&
                 ty31 == ty12 &&
                 ty22 == ty32 then return ty32 else Nothing
            _ -> Nothing
        _ -> Nothing
    _ -> Nothing
getType gamma (TermNeg tm1) = do
  ty1 <- getType gamma tm1
  case ty1 of
    TypeImp ty11 TypeFalse -> return (TypeNeg ty11)
    _ -> Nothing


{-
Examples:

1. [HP : P, HQ : Q] |- HP : P ; Var
2. [HP : P] |- \HQ => HP : Q -> P ; Abs 1
3. [] |- \HP => (\HQ => HP) : P -> (Q -> P) ; Abs 2

\HP : P => (\HQ : Q => HP)
P -> (Q -> P)

*Main> getType (Data.Map.fromList []) (TermImpIntro "HP" (TypeVar "P") (TermImpIntro "HQ" (TypeVar "Q") (TermVar "HP")))
Just (TypeImp (TypeVar "P") (TypeImp (TypeVar "Q") (TypeVar "P")))

-}

[Mario Carneiro]

Looks good. You are missing TermNegElim though, or however you want to call it. It does the reverse of TermNeg: if tm : !P then TermNegElim tm : P -> False

[Mario Carneiro]

alternatively, you can have a rule that Absurd h1 h2 : False if h1 : !P and h2 : P

[Mario Carneiro]

or you can just define TypeNeg T = TypeImp T False which is what lean does

[Patrick Thomas]

Thank you!

[Mario Carneiro]

Regarding FOL, you can do that here using TypeForall String Type which is \all x, P[x] and TermForallIntro String Term which is like \lam x, e[x] but introduces another kind of variable. TermForallElim Term String takes a proof of \all x, P[x] and y and produces P[y]

[Mario Carneiro]

This is assuming you want pure FOL, not HOL where the forall would have variables which range over regular types

[Mario Carneiro]

In this case, that would mean that they can only range over propositions

[Patrick Thomas]

I thought in FOL you had some domain of discourse that the variables ranged over, other than propositions?

[Patrick Thomas]

and predicates took those variables to propositions.

[Mario Carneiro]

right, TypeForall is like \all x : D, P[x] where D is the domain of discourse, which acts like a fake type here

[Mario Carneiro]

so you have a split context, with variables for propositions and variables over the domain of discourse

[Patrick Thomas]

Oh. I think I see. Does that mean you actually need an additional map for a second context?

[Mario Carneiro]

yes

[Patrick Thomas]

Ok.

[Mario Carneiro]

you can also share the map and have the map value be Either Type Unit

[Mario Carneiro]

the difference is whether you allow hypotheses and variables with the same "namespace" where they can shadow each other or not

[Patrick Thomas]

Is Unit the type in Haskell that is uninhabited or something like that? Here it would represent the domain of discourse D?

[Mario Carneiro]

It's the type with one element

[Mario Carneiro]

I think it's called unit

[Mario Carneiro]

you can use Maybe Type too if that isn't confusing to you

[Patrick Thomas]

You're probably right. I was guessing.

[Mario Carneiro]

oh, sorry it's spelled () in haskell

[Patrick Thomas]

No problem.

[Patrick Thomas]

I'll see if I can add it another night. Thank you!

[Patrick Thomas]

(deleted)

[Patrick Thomas]

I'm not sure what to return for TermForAllElim. Do I need to add a type like TypeApp Type String? And a type like TypeVar' for variables that range over the domain of discourse?

-- Modified from https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html

import Data.Map


-- Proposition
data Type = TypeVar String -- Propositional variables. (P, Q, etc.)
          | TypeTrue
          | TypeFalse
          | TypeImp Type Type
          | TypeAnd Type Type
          | TypeOr Type Type
          | TypeNeg Type
          | TypeForAll String Type -- \forall x, P[x]. String is the name of a variable that ranges over some domain of discourse. (x, y, etc.) Type is the proposition formed from substituting some element in the domain of discourse into some predicate. (P[x], P[y], etc.)
            deriving (Eq, Show)

-- Proof
data Term = TermVar String -- Hypothesis
          | TermTriv
          | TermExFalso Type
          | TermImpIntro String Type Term -- Abstraction
          | TermImpElim Term Term -- Application
          | TermAndIntro Term Term
          | TermAndElimLeft Term
          | TermAndElimRight Term
          | TermOrIntroLeft Term Type
          | TermOrIntroRight Type Term
          | TermOrElim Term Term Term
          | TermNegIntro Term
          | TermNegElim Term
          | TermForAllIntro String Term
--          | TermForAllElim Term String
            deriving (Eq, Show)


-- String is the name of an assumption that some proposition holds.
-- Type is the proposition that is being assumed to hold.
type ContextH = Data.Map.Map String Type

-- String is the name of a variable assumed to range over some domain of discourse.
type ContextD = [String]


getType :: ContextH -> ContextD -> Term -> Maybe Type

-- x is the name of an arbitrary element in the domain of discourse.
-- tm1 is the proof of the proposition formed from substituting x into some predicate P.
getType gamma_h gamma_d (TermForAllIntro x tm1) =
  let gamma_d' = x : gamma_d in do
    -- ty1 is the proposition formed from substituting x into some predicate P. (P[x])
    ty1 <- getType gamma_h gamma_d' tm1
    return (TypeForAll x ty1)
{-
getType gamma_h gamma_d (TermForAllElim tm1 y) =
  if elem y gamma_d then do
    ty1 <- getType gamma_h gamma_d tm1
    case ty1 of
      TypeForAll x ty11 -> return ?
      _ -> Nothing
  else Nothing
-}
getType gamma_h _ (TermVar v) = Data.Map.lookup v gamma_h

getType _ _ TermTriv = return TypeTrue

getType _ _ (TermExFalso ty) = return (TypeImp TypeFalse ty)

getType gamma_h gamma_d (TermImpIntro v tyv tm1) =
  let gamma_h' = Data.Map.insert v tyv gamma_h in do
    ty1 <- getType gamma_h' gamma_d tm1
    return (TypeImp tyv ty1)

getType gamma_h gamma_d (TermImpElim tm1 tm2) = do
  ty1 <- getType gamma_h gamma_d tm1
  ty2 <- getType gamma_h gamma_d tm2
  case ty1 of
    TypeImp ty11 ty12 -> if ty11 == ty2 then return ty12 else Nothing
    _ -> Nothing

getType gamma_h gamma_d (TermAndIntro tm1 tm2) = do
  ty1 <- getType gamma_h gamma_d tm1
  ty2 <- getType gamma_h gamma_d tm2
  return (TypeAnd ty1 ty2)

getType gamma_h gamma_d (TermAndElimLeft tm1) = do
  ty1 <- getType gamma_h gamma_d tm1
  case ty1 of
    TypeAnd ty11 _ -> return ty11
    _ -> Nothing

getType gamma_h gamma_d (TermAndElimRight tm1) = do
  ty1 <- getType gamma_h gamma_d tm1
  case ty1 of
    TypeAnd _ ty12 -> return ty12
    _ -> Nothing

getType gamma_h gamma_d (TermOrIntroLeft tm1 ty2) = do
  ty1 <- getType gamma_h gamma_d tm1
  return (TypeOr ty1 ty2)

getType gamma_h gamma_d (TermOrIntroRight ty1 tm2) = do
  ty2 <- getType gamma_h gamma_d tm2
  return (TypeOr ty1 ty2)

getType gamma_h gamma_d (TermOrElim tm1 tm2 tm3) = do
  ty1 <- getType gamma_h gamma_d tm1
  ty2 <- getType gamma_h gamma_d tm2
  ty3 <- getType gamma_h gamma_d tm3
  case ty1 of
    TypeOr ty11 ty12 ->
      case ty2 of
        TypeImp ty21 ty22 ->
          case ty3 of
            TypeImp ty31 ty32 ->
              if ty21 == ty11 &&
                 ty31 == ty12 &&
                 ty22 == ty32 then return ty32 else Nothing
            _ -> Nothing
        _ -> Nothing
    _ -> Nothing

getType gamma_h gamma_d (TermNegIntro tm1) = do
  ty1 <- getType gamma_h gamma_d tm1
  case ty1 of
    TypeImp ty11 TypeFalse -> return (TypeNeg ty11)
    _ -> Nothing

getType gamma_h gamma_d (TermNegElim tm1) = do
  ty1 <- getType gamma_h gamma_d tm1
  case ty1 of
    TypeNeg ty11 -> return (TypeImp ty11 TypeFalse)
    _ -> Nothing


{-
Examples:

1. [HP : P, HQ : Q] |- HP : P ; Var
2. [HP : P] |- \HQ => HP : Q -> P ; Abs 1
3. [] |- \HP => (\HQ => HP) : P -> (Q -> P) ; Abs 2

\HP : P => (\HQ : Q => HP)
P -> (Q -> P)

*Main> getType (Data.Map.fromList []) (TermImpIntro "HP" (TypeVar "P") (TermImpIntro "HQ" (TypeVar "Q") (TermVar "HP")))
Just (TypeImp (TypeVar "P") (TypeImp (TypeVar "Q") (TypeVar "P")))

-}

[Patrick Thomas]

(deleted)

[Mario Carneiro]

Suggestion: you can define type Context = (ContextH, ContextD) and that way you don't need two gamma variables everywhere

[Patrick Thomas]

Good point.

[Mario Carneiro]

For the type of TermForAllElim, you should return subst x y P, meaning to replace free occurrences of x with y

[Mario Carneiro]

so you have to define that function

[Mario Carneiro]

There isn't really anything to substitute though, since there is no way to put a domain variable in a type right now

[Mario Carneiro]

so you need something like TypePred String String representing R(x) where R is an uninterpreted constant

[Mario Carneiro]

that way you can construct types like all x, P(x) -> !P(y)

[Patrick Thomas]

I guess I'm confused why I need to define that substitution function, but not the one for the term application?

[Patrick Thomas]

Or are you saying I actually don't need it?

[Mario Carneiro]

you will need substitution at the term level as well, if you want to reduce lambda terms instead of just typechecking them

[Patrick Thomas]

Right now I'm just looking at type checking.

[Mario Carneiro]

there isn't any lambda calculus at the type level (yet...) so app would just get in the way

[Patrick Thomas]

So to just do type checking all I need to do is add TypePred String String?

[Mario Carneiro]

for example, if you defer the substitution, then you go from all x, P(x) /\ Q(x) to (P(x) /\ Q(x))[y/x] and now you can't use and.left anymore because the substitution is in the way

[Patrick Thomas]

Oh.

[Mario Carneiro]

you don't actually need TypePred, but without it subst will be trivial, subst x y P = P

[Mario Carneiro]

basically there is no way right now to write P(x) so you can build types like all x, P /\ Q which substitutes to P /\ Q. True, but not very interesting

[Patrick Thomas]

So for that I need TypePred.

[Mario Carneiro]

right, that's the P(x) I'm writing

[Patrick Thomas]

I see.

[Mario Carneiro]

you want all x, P(x) /\ Q(x)to substitute to P(y) /\ Q(y), and subst will traverse the term to replace x with y

[Mario Carneiro]

but you have to be careful about binders: all x, (all x, P(x)) /\ Q(x) should substitute to (all x, P(x)) /\ Q(y)

[Patrick Thomas]

So in TermForAllElim what happens if I return TypePred?

[Mario Carneiro]

well TypePred here is for an atomic predicate, in general TermForAllElim can return a composite term like P(y) /\ Q(y)

[Patrick Thomas]

I see.

[Mario Carneiro]

it can be seen as a replacement for TypeVar now that we are doing predicate calculus instead of propositional calc

[Mario Carneiro]

so we need predicates

[Patrick Thomas]

Yep.

[Patrick Thomas]

What part of the lambda cube is this, or is it on the lambda cube?

[Mario Carneiro]

people also sometimes allow n-ary predicates like P(x, y, z) with the 0-ary case being propositional variables

[Patrick Thomas]

I'm guessing it is no longer STLC?

[Mario Carneiro]

it's a bit off the beaten track: we have types that bind D-variables and terms that H-bind types, but the two categories are separated so it's not as powerful as lambda-P2

[Mario Carneiro]

notice what it says here:

The conversion rule is strongly needed when dealing with dependent types, because it allows to perform computation on the terms in the type. For instance, if you have Γ ⊢ A : P ( ( λ x . x ) y ) and Γ ⊢ B : Π x : P ( y ) . C, you need to apply the conversion rule to obtain Γ ⊢ A : P ( y ) to be able to type Γ ⊢ B A : C.

For the moment we're getting around this by not having D-terms

[Mario Carneiro]

which is enough to do pure predicate calculus, and you can even do ZFC without needing any terms inside predicates (although you need at least one binary relation, unary predicates don't cut it)

[Patrick Thomas]

Are D terms like functions in FOL? Like there are predicates that take elements of D to Prop and functions that take elements of D to elements of D?

[Mario Carneiro]

An example of a D term in FOL is x + y in peano arithmetic

[Mario Carneiro]

so + is a term constructor, we would say it has type D -> D -> D

[Mario Carneiro]

predicates are things like =, which has type D -> D -> Prop

[Mario Carneiro]

In classical predicate logic you usually have predicates like = and then maybe term constructors like +

[Mario Carneiro]

0 is also considered a 0-ary term constructor in PA

[Mario Carneiro]

ZFC has no term constructors and only one predicate, x \in y

[Mario Carneiro]

sometimes = is also included but you can define it in terms of \in

[Patrick Thomas]

Oh. Right. The domain of discourse is sets.

[Patrick Thomas]

Did you mean lambda P above instead of lambda P2?

[Patrick Thomas]

The quote is from lambda P I think?

[Patrick Thomas]

I guess I'm wondering, from a learning perspective, if I should continue expanding this or jump to the next simplest on the way to CIC, which I guess is lambda P?

[Patrick Thomas]

In which systems in the lambda cube do the terms and types get combined into one data type?

[Mario Carneiro]

only lambda-C aka CoC combines the two

[Mario Carneiro]

anywhere below that, you need terms and types to be separate to even be able to state the dependency relations

[Patrick Thomas]

What would my formulation look like for lambda P? https://en.wikipedia.org/wiki/Lambda_cube#(%CE%BBP)_Lambda-P

[Patrick Thomas]

Is this correct for the untyped lambda calculus using named variables? What is the usual way to automate the alpha renaming when it is needed in substitution?

import Data.List
import Data.Set


data Term = Var String | App Term Term | Abs String Term
  deriving (Eq, Show)


getSubTermList :: Term -> [Term]
getSubTermList t@(Var _)   = [t]
getSubTermList t@(App m n) = (getSubTermList m) ++ (getSubTermList n) ++ [t]
getSubTermList t@(Abs _ m) = (getSubTermList m) ++ [t]

getProperSubTermList :: Term -> [Term]
getProperSubTermList t = Data.List.delete t (getSubTermList t)


getFreeVariableSet :: Term -> Data.Set.Set String
getFreeVariableSet (Var x)   = Data.Set.singleton x
getFreeVariableSet (App m n) =
  Data.Set.union (getFreeVariableSet m) (getFreeVariableSet n)
getFreeVariableSet (Abs x m) =
  Data.Set.difference (getFreeVariableSet m) (Data.Set.singleton x)

isClosedTerm :: Term -> Bool
isClosedTerm t = Data.Set.null (getFreeVariableSet t)


getBindingVariableSet :: Term -> Data.Set.Set String
getBindingVariableSet (Var _)   = Data.Set.empty
getBindingVariableSet (App m n) =
  Data.Set.union (getBindingVariableSet m) (getBindingVariableSet n)
getBindingVariableSet (Abs x m) =
  Data.Set.union (getBindingVariableSet m) (Data.Set.singleton x)


replaceFree :: String -> String -> Term -> Term
replaceFree u v (Var x)   =
  if u == x then (Var v) else (Var x)
replaceFree u v (App m n) =
  App (replaceFree u v m) (replaceFree u v n)
replaceFree u v (Abs x m) =
  if u == x then (Abs x m) else (Abs x (replaceFree u v m))

alphaReplace :: String -> String -> Term -> Term
alphaReplace u v (Abs x m) = if u == x
                             && Data.Set.notMember v (getFreeVariableSet m)
                             && Data.Set.notMember v (getBindingVariableSet m)
                             then Abs v (replaceFree u v m)
                             else error "bad input"
alphaReplace _ _ _         = error "bad input"


-- substitute m x n = m [ x := n ]
substitute :: Term -> String -> Term -> Term
substitute (Var y) x n   = if x == y then n else (Var y)
substitute (App p q) x n = App (substitute p x n) (substitute q x n)
substitute (Abs y p) x n
  | x == y = Abs y p
  | x /= y && Data.Set.notMember x (getFreeVariableSet (Abs y p)) =
      Abs y (substitute p x n)
  | x /= y && Data.Set.notMember y (getFreeVariableSet n) =
      Abs y (substitute p x n)
  | otherwise = error "bad input"


betaReduce :: Term -> Term
betaReduce (App (Abs x m) n) = substitute m x n
betaReduce _                 = error "bad input"

[Patrick Thomas]

Is this right?

-- untyped lambda calculus using De Bruijn indexing

-- Modified from https://www.cs.cornell.edu/courses/cs4110/2018fa/lectures/lecture15.pdf


data Term = Var Int | App Term Term | Abs Term
  deriving (Eq, Show)

{-
De Bruijn | Named Variable
Abs (Var 0) = Abs "x" (Var "x")
Abs (Var 1) = Abs "x" (Var "y")
Abs (Abs (Var 0)) = Abs "x" (Abs "y" (Var "y"))
Abs (Abs (Var 1)) = Abs "x" (Abs "y" (Var "x"))
Abs (Abs (Var 2)) = Abs "x" (Abs "y" (Var "z"))
-}

{-
shift t c i = Shifts the indices of the free variables in a term t above a
cutoff c up by i.
-}
shift :: Term -> Int -> Int -> Term
shift (Var n)     c i = if n < c then Var n else Var (n + i)
shift (App e1 e2) c i = App (shift e1 c i) (shift e2 c i)
shift (Abs e)     c i = Abs (shift e (c + 1) i)

{-
Each time a lambda is gone under the index of the variable being substituted
for is increased by one and the free variables in the expression being
substituted in are shifted up by one. The free variables in the expression
being substituted in are shifted up by one so that they do not become captured
by the binding variables above the variable being substituted for.
-}
substitute :: Term -> Int -> Term -> Term
substitute (Var y)     x n = if x == y then n else Var y
substitute (App e1 e2) x n = App (substitute e1 x n) (substitute e2 x n)
substitute (Abs e)     x n = Abs (substitute e (x + 1) (shift n 0 1))

{-
Substitutes occurrences of 0, the index of the variable being bound by the
lambda, by e2 shifted up by one. Then shifts the result down by one to ensure
that any free variables in e1 continue to refer to the same things after the
lambda is removed.
-}
betaReduce :: Term -> Term
betaReduce (App (Abs e1) e2) = shift (substitute e1 0 (shift e2 0 1)) 0 (-1)
betaReduce _                 = error "bad input"

[Patrick Thomas]

Is this right for the second order typed lambda calculus using named variables? If all of the variables names in the context and given term are required to differ, does that avoid the need for alpha renaming?

-- second order typed lambda calculus using named variables

import Data.Set
import Data.Map


data Type = TypeVar String -- V
          | TypeArrow Type Type -- Type -> Type
          | TypePi String Type -- Pi V : * . Type
            deriving (Show, Eq)

data Term = TermVar String -- V'
          | TermApp Term Term -- Term Term
          | TermAbs String Type Term -- \lambda V' : Type . Term
          | TermTypeApp Term Type -- Term Type
          | TermTypeAbs String Term -- \lambda V : * . Term
            deriving (Show, Eq)


getFreeTypeVariableSet :: Type -> Data.Set.Set String
getFreeTypeVariableSet (TypeVar x)     = Data.Set.singleton x
getFreeTypeVariableSet (TypeArrow m n) =
  Data.Set.union (getFreeTypeVariableSet m) (getFreeTypeVariableSet n)
getFreeTypeVariableSet (TypePi x m)    =
  Data.Set.difference (getFreeTypeVariableSet m) (Data.Set.singleton x)


-- substitute m x n = m [ x := n ]
substitute :: Type -> String -> Type -> Type
substitute (TypeVar y) x n = if x == y then n else (TypeVar y)
substitute (TypeArrow p q) x n = TypeArrow (substitute p x n) (substitute q x n)
substitute (TypePi y p) x n
  | x == y = TypePi y p
  | x /= y && Data.Set.notMember x (getFreeTypeVariableSet (TypePi y p)) =
      TypePi y (substitute p x n)
  | x /= y && Data.Set.notMember y (getFreeTypeVariableSet n) =
      TypePi y (substitute p x n)
  | otherwise = error "bad input"


type TermContext = Data.Map.Map String Type
type TypeContext = Data.Set.Set String -- String : *


getType :: TermContext -> TypeContext -> Term -> Maybe Type

{-
(var)
\Gamma |- x : \sigma if x : \sigma \in Gamma
-}
getType term_gamma _ (TermVar x) = Data.Map.lookup x term_gamma

{-
(appl)
\Gamma |- M : \sigma -> \tau  \Gamma |- N : \sigma
--------------------------------------------------
            \Gamma |- M N : \tau
-}
getType term_gamma type_gamma (TermApp m n) = do
  ty_m <- getType term_gamma type_gamma m
  ty_n <- getType term_gamma type_gamma n
  case ty_m of
    TypeArrow sigma tau -> if ty_n == sigma then return tau else Nothing
    _ -> Nothing

{-
(abst)
         \Gamma, x : \sigma |- M : \tau
-------------------------------------------------
\Gamma |- \lambda x : \sigma . M : \sigma -> \tau
-}
getType term_gamma type_gamma (TermAbs x sigma m) =
  if Data.Map.notMember x term_gamma &&
     Data.Set.notMember x type_gamma &&
     (getFreeTypeVariableSet sigma) `Data.Set.isSubsetOf` type_gamma
  then
     let term_gamma' = Data.Map.insert x sigma term_gamma in do
     tau <- getType term_gamma' type_gamma m
     return (TypeArrow sigma tau)
  else Nothing

{-
(appl_2)
\Gamma |- M : (Pi \alpha : * . A)  \Gamma |- B : *
--------------------------------------------------
          \Gamma |- M B : A [\alpha := B]
-}
getType term_gamma type_gamma (TermTypeApp m b) =
  if (getFreeTypeVariableSet b) `Data.Set.isSubsetOf` type_gamma
  then do
    ty_m <- getType term_gamma type_gamma m
    case ty_m of
      TypePi alpha a -> return (substitute a alpha b)
      _ -> Nothing
  else Nothing

{-
(abst_2)
          \Gamma, \alpha : * |- M : A
----------------------------------------------------
\Gamma |- \lambda \alpha : * . M : Pi \alpha : * . A
-}
getType term_gamma type_gamma (TermTypeAbs alpha m) =
  if Data.Map.notMember alpha term_gamma &&
     Data.Set.notMember alpha type_gamma
  then
    let type_gamma' = Data.Set.insert alpha type_gamma in do
    a <- getType term_gamma type_gamma' m
    return (TypePi alpha a)
  else Nothing


{-
Example:

*Main> getType Data.Map.empty (Data.Set.singleton "nat") (TermTypeApp (TermTypeAbs "alpha" (TermAbs "f" (TypeArrow (TypeVar "alpha") (TypeVar "alpha")) (TermAbs "x" (TypeVar "alpha") (TermApp (TermVar "f") (TermApp (TermVar "f") (TermVar "x")))))) (TypeVar "nat"))
Just (TypeArrow (TypeArrow (TypeVar "nat") (TypeVar "nat")) (TypeArrow (TypeVar "nat") (TypeVar "nat")))
-}

[Patrick Thomas]

Sorry, just wondering if anyone could help with the above questions.

[Mario Carneiro]

If all of the variables names in the context and given term are required to differ, does that avoid the need for alpha renaming?

Unfortunately not, because terms can end up duplicated by substitution and beta reduction can end up requiring you to nest a term inside itself

[Mario Carneiro]

What is the usual way to automate the alpha renaming when it is needed in substitution?

I recall the HOL light implementation will just keep putting ' on the variable name until it is not in the context anymore

[Patrick Thomas]

Thank you! Does what I have for the De Bruijn indexing look right?

[Mario Carneiro]

substitute isn't quite right. What you want is a function that maps subst (var i) k e = if i < k then var i else if i == k then e else var (i-1)

[Mario Carneiro]

that is, all variables above the cutoff are decreased by 1

[Mario Carneiro]

there is also a generalized version of this where you substitute a list of values of length n into variables k, k+1, ..., k+n-1 and shift everything above that down by n

[Mario Carneiro]

but you don't need that for basic lambda calculus, unless you optimize for the case of substituting multiple lambdas at once

[Mario Carneiro]

then in betaReduce you won't need to shift _ 0 (-1)

[Patrick Thomas]

Are you saying it should be:

-- untyped lambda calculus using De Bruijn indexing

-- Modified from https://www.cs.cornell.edu/courses/cs4110/2018fa/lectures/lecture15.pdf


data Term = Var Int | App Term Term | Abs Term
  deriving (Eq, Show)

{-
De Bruijn | Named Variable
Abs (Var 0) = Abs "x" (Var "x")
Abs (Var 1) = Abs "x" (Var "y")
Abs (Abs (Var 0)) = Abs "x" (Abs "y" (Var "y"))
Abs (Abs (Var 1)) = Abs "x" (Abs "y" (Var "x"))
Abs (Abs (Var 2)) = Abs "x" (Abs "y" (Var "z"))
-}

{-
shift t c i = Shifts the indices of the free variables in a term t above a
cutoff c up by i.
-}
shift :: Term -> Int -> Int -> Term
shift (Var n)     c i = if n < c then Var n else Var (n + i)
shift (App e1 e2) c i = App (shift e1 c i) (shift e2 c i)
shift (Abs e)     c i = Abs (shift e (c + 1) i)

{-
Each time a lambda is gone under the index of the variable being substituted
for is increased by one and the free variables in the expression being
substituted in are shifted up by one. The free variables in the expression
being substituted in are shifted up by one so that they do not become captured
by the binding variables above the variable being substituted for.
-}
substitute :: Term -> Int -> Term -> Term
substitute (Var y)     x n = if y < x then Var y else if x == y then n else Var (y - 1)
substitute (App e1 e2) x n = App (substitute e1 x n) (substitute e2 x n)
substitute (Abs e)     x n = Abs (substitute e (x + 1) (shift n 0 1))

{-
Substitutes occurrences of 0, the index of the variable being bound by the
lambda, by e2 shifted up by one. Then shifts the result down by one to ensure
that any free variables in e1 continue to refer to the same things after the
lambda is removed.
-}
betaReduce :: Term -> Term
betaReduce (App (Abs e1) e2) = substitute e1 0 (shift e2 0 1)
betaReduce _                 = error "bad input"

[Mario Carneiro]

you shouldn't need (substitute e (x + 1) (shift n 0 1)) in the Abs case, it should just be substitute e (x + 1) n

[Mario Carneiro]

oh wait, no you do need that

[Mario Carneiro]

you can also not shift there and shift by x in the Var case, although it's a toss-up which is more efficient

[Patrick Thomas]

Were you saying that the beta reduce would not work correctly in the original version, or that it was just not the usual implementation?

[Patrick Thomas]

I'm not sure I understand what the change does.

[Patrick Thomas]

If I translate this into Lean, what do I need to prove to ensure that it is correct?

[Mario Carneiro]

Patrick Thomas said:

Were you saying that the beta reduce would not work correctly in the original version, or that it was just not the usual implementation?

It's not the usual implementation. In particular, the revised version means that you never have to worry about negative shifts, which are problematic to reason about because they might produce negative variables and/or overlap variables

[Mario Carneiro]

you can think of substitute as a rearrangement of indices that removes x from the list (substituting the variable there) and shifts other indexes around so that no indexes are left stranded

[Mario Carneiro]

you can even type check these operations as context -> context functions that insert or remove an element from the middle of the list

[Mario Carneiro]

Patrick Thomas said:

If I translate this into Lean, what do I need to prove to ensure that it is correct?

The main theorem you want to prove about these operations is type correctness: if Gamma |- e : A then Gamma, B |- lift e 0 1 : A, and if Gamma, B |- f : A and Gamma |- x : B then Gamma |- substitute f 0 x : B

[Mario Carneiro]

if you have dependent types then the first theorem is actually Gamma |- e : A => Gamma, B |- lift e 0 1 : lift A 0 1

[Mario Carneiro]

and of course these theorems generalize when the indices are not just 0 and 1, which you will need when proving them by induction

[Patrick Thomas]

In the source I translated the code from it stated:

Then shifts the result down by one to ensure
that any free variables in e1 continue to refer to the same things after the
lambda is removed.

How is this ensured in the revision?

[Mario Carneiro]

it is done by substitute in the high-var case

[Mario Carneiro]

substituting (#1 + #0)[e/#0] is (#0 + e)

[Mario Carneiro]

essentially, we think of the substitution operation itself being a kind of binder, so variables above the substitution target are actually referring to numbers one less in the outer context

[Mario Carneiro]

you can see that from the typing theorem I gave for substitute: if substitute f 0 x exists in context Gamma then f is in context Gamma, B, which is to say that variable 0 refers to B and variables 1 and up refer to things in Gamma

[Mario Carneiro]

If you don't do that shift then you have the more awkward typing theorem that if Gamma, B |- f : A and Gamma |- x : B then Gamma, INVALID |- substitute f 0 x : B where INVALID means that this variable should not be referred to in the term

[Mario Carneiro]

and you later fix that up with a shift _ 0 (-1), which only has a partial typing theorem: if Gamma, INVALID |- e : A then Gamma |- shift e 0 (-1) : A

[Patrick Thomas]

I'm sorry, I'm not sure I see how Var (y - 1) in substitute has any affect on the variables in n (e2 in betaReduce)?

[Patrick Thomas]

Should the shift be removed from the betaReduce function in the revised version? That is, substitute e1 0 e2?

[Patrick Thomas]

Like this?

-- untyped lambda calculus using De Bruijn indexing


data Term = Var Int | App Term Term | Abs Term
  deriving (Eq, Show)

{-
De Bruijn | Named Variable
Abs (Var 0) = Abs "x" (Var "x")
Abs (Var 1) = Abs "x" (Var "y")
Abs (Abs (Var 0)) = Abs "x" (Abs "y" (Var "y"))
Abs (Abs (Var 1)) = Abs "x" (Abs "y" (Var "x"))
Abs (Abs (Var 2)) = Abs "x" (Abs "y" (Var "z"))
-}

{-
lift t c = Increases the indices of the free variables in a term t above a
cutoff c by one.
-}
lift :: Term -> Int -> Term
lift (Var n)     c = if n < c then Var n else Var (n + 1)
lift (App e1 e2) c = App (lift e1 c) (lift e2 c)
lift (Abs e)     c = Abs (lift e (c + 1))

{-
Each time a lambda is gone under the index of the variable being substituted
for is increased by one and the indices of the free variables in the term being
substituted in are increased by one. The indices of the free variables in the
term being substituted in are increased by one so that they do not become
captured by the binding variables above the variable being substituted for.
The indices of the free variables in the term being substituted into are
decreased by one because the substitution is intended to be used for defining
beta reduction and a lambda disappears in the beta reduction process.
-}
substitute :: Term -> Int -> Term -> Term
substitute (Var y)     x n = if y < x then Var y else if x == y then n else Var (y - 1)
substitute (App e1 e2) x n = App (substitute e1 x n) (substitute e2 x n)
substitute (Abs e)     x n = Abs (substitute e (x + 1) (lift n 0))

betaReduce :: Term -> Term
betaReduce (App (Abs e1) e2) = substitute e1 0 e2
betaReduce _                 = error "bad input"

[Patrick Thomas]

Mario Carneiro said:

Yes. Lean uses a combination of named and de bruijn variables called "locally nameless": variables inside a term are de bruijn, but binders are "opened" when they enter the local context, at which point they are replaced with "local constants" that are basically named variables

Is this what you mean? Is this right?

-- The untyped lambda calculus using locally nameless bindings.

-- Adapted from https://boarders.github.io/posts/locally-nameless/


import Data.List
import Data.Map


-- named variable
data Term a = Var a
            | App (Term a) (Term a)
            | Abs a (Term a)
              deriving (Eq, Show)

data Var a = F a   -- The name of a free variable or a binding variable.
           | B Int -- The De Bruijn index of a bound variable.
             deriving (Eq, Show)

-- locally nameless
type TermLN a = Term (Var a)


{-
Translates a named variable term to a locally nameless term.
Keeps the name of each free variable and binding variable. Changes the name of
each bound variable to its De Bruijn index.
-}
toLN :: (Ord a) => Term a -> TermLN a
toLN t = go Data.Map.empty t
  where
    {-
    The mapping is from the name of each binding variable to its De Bruijn
    index at the current depth.
    -}
    go :: (Ord a) => Data.Map.Map a Int -> Term a -> TermLN a
    go env (Var name)   =
      case name `Data.Map.lookup` env of
        {-
        The variable name is a key in the map. Therefore it has the same name
        as a binding variable. Therefore it is a bound variable. Then the
        De Bruijn index of the binding variable it matches is used.
        -}
        Just index -> Var (B index)
        {-
        The variable name is not a key in the map. Therefore it is a free
        variable. Then its name is kept.
        -}
        Nothing    -> Var (F name)
    go env (App t1 t2)  = App (go env t1) (go env t2)
    go env (Abs name t) =
      {-
      Since a binding variable has been gone under, the De Bruijn index of
      each binding variable at the current depth is increased by 1 and the
      De Bruijn index of the encountered binding variable at the current
      depth is set to 0.
      -}
      let env' = Data.Map.insert name 0 (Data.Map.map (+1) env) in
      Abs (F name) (go env' t) -- The name of the binding variable is kept.


-- Translates a locally nameless term to a named variable term.
fromLN :: (Ord a) => TermLN a -> Term a
fromLN t = go Data.Map.empty t
  where
    {-
    The mapping is from the De Bruijn index of each binding variable at the
    current depth to its name.
    -}
    go :: (Ord a) => Data.Map.Map Int a -> TermLN a -> Term a
    go env (Var v)     =
      case v of
        -- This is a free variable.
        F name  -> Var name
        -- This is a bound variable.
        B index -> case index `Data.Map.lookup` env of
                     Just name -> Var name
                     Nothing   -> error "Bound variable has no binder."
    go env (App t1 t2) = App (go env t1) (go env t2)
    go env (Abs v t)   =
      case v of
        B _    -> error "Bound variable at binding site."
        {-
        Since a binding variable has been gone under, the
        De Bruijn index of each binding variable at the
        current depth is increased by 1 and the De Bruijn
        index of the encountered binding variable at the
        current depth is set to 0.
        -}
        F name -> let env' = Data.Map.insert 0 name (Data.Map.mapKeysMonotonic (+1) env) in
                             Abs name (go env' t)


{-
substitute m n = Computes (Abs x m) [x := n].
-}
substitute :: TermLN a -> TermLN a -> TermLN a
substitute m n = go 0 m n
  where
    go :: Int -> TermLN a -> TermLN a -> TermLN a
    go outer (Var v) n =
      case v of
        {-
        If the bound variable refers to the outermost binder of the body then
        the bound variable is replaced by n.
        -}
        B index -> if index == outer then n else Var (B index)
        F name -> Var (F name)
    go outer (App t1 t2) n = App (go outer t1 n) (go outer t2 n)
    {-
    Since a binding variable has been gone under, the index of the bound
    variable to be replaced must be increased so that it continues to refer
    to the outermost binder.
    -}
    go outer (Abs v t) n = Abs v (go (outer + 1) t n)


-- Converts a locally nameless term to weak head normal form.
whnfLN :: TermLN a -> TermLN a
whnfLN t = go t []
  where
    go :: TermLN a -> [TermLN a] -> TermLN a
    go (App t1 t2) args = go t1 (t2 : args)
    go (Abs _ t) (a : args) = go (substitute t a) args
    go t args = Data.List.foldl' App t args

-- Converts a named variable term to weak head normal form.
whnf :: (Ord a) => Term a -> Term a
whnf = fromLN . whnfLN . toLN


-- Converts a locally nameless term to normal form.
nfLN :: TermLN a -> TermLN a
nfLN t = go t []
  where
    go :: TermLN a -> [TermLN a] -> TermLN a
    go (App t1 t2) args = go t1 (t2 : args)
    go (Abs v t) [] = Abs v (nfLN t)
    go (Abs _ t) (a : args) = go (substitute t a) args
    go t args = Data.List.foldl' App t (fmap nfLN args)

-- Converts a named variable term to normal form.
nf :: (Ord a) => Term a -> Term a
nf = fromLN . nfLN . toLN

[Patrick Thomas]

Are these the correct terms and types for \lambda \underline{\omega} (types that depend on other types)?

data Square = SquareSquare
  deriving (Show, Eq)

data Kind = KindStar
          | KindArrow Kind Kind
            deriving (Show, Eq)

data Type = TypeVar String           -- V
          | TypeArrow Type Type      -- Type -> Type
          | TypeApp Type Type        -- Type Type
          | TypeAbs String Kind Type -- \lambda V : Kind . Type
            deriving (Show, Eq)

data Term = TermVar String           -- V'
          | TermApp Term Term        -- Term Term
          | TermAbs String Type Term -- \lambda V' : Type . Term
            deriving (Show, Eq)


data Declaration = TermDeclaration (String, Type)
                 | TypeDeclaration (String, Kind)

type Context = [Declaration]

[Mario Carneiro]

You also want a big-lambda operator in the term language, as the inhabitants of TypeAbs

[Patrick Thomas]

Can you suggest a good reference for what I am trying to do? I'm using Type Theory and Formal Proof by Rob Nederpelt and Herman Geuvers but it wasn't clear on this language syntax.

[Patrick Thomas]

I think maybe you are referring to what is titled here [1] as λω (System F-omega) and I am referring to what is titled λω_ (STLC + higher-kinded type operators)?
[1] https://cstheory.stackexchange.com/questions/36054/how-do-you-get-the-calculus-of-constructions-from-the-other-points-in-the-lambda

[Patrick Thomas]

How do you deal with the weakening rule when writing a type checker for λω_ (STLC + higher-kinded type operators) when it seems that its conclusion can mirror the conclusion of other rules?

[Patrick Thomas]

This is my attempt that I'm not sure how to fix:

-- underscore omega (STLC + type constructors)


data Square = SquareSquare
  deriving (Show, Eq)

data Kind = KindStar
          | KindArrow Kind Kind
            deriving (Show, Eq)

data Type = TypeVar String           -- V
          | TypeArrow Type Type      -- Type -> Type
          | TypeApp Type Type        -- Type Type
          | TypeAbs String Kind Type -- \lambda V : Kind . Type
            deriving (Show, Eq)

data Term = TermVar String           -- V'
          | TermApp Term Term        -- Term Term
          | TermAbs String Type Term -- \lambda V' : Type . Term
            deriving (Show, Eq)


data Declaration = TermDeclaration (String, Type)
                 | TypeDeclaration (String, Kind)

type Context = [Declaration]

getDomain :: Context -> [String]
getDomain []                                   = []
getDomain (TermDeclaration (x, _) : gamma)     = x : (getDomain gamma)
getDomain (TypeDeclaration (alpha, _) : gamma) = alpha : (getDomain gamma)


-- getSquare

getSquare :: Context -> Kind -> Maybe Square

{-
(sort)
\empty |- * : Square
-}
getSquare [] KindStar = Just SquareSquare

{-
* -> * : Square
* -> (* -> *) : Square

(form) (s = square)
\Gamma |- A : s  \Gamma |- B : s
--------------------------------
     \Gamma |- A -> B : s
-}
getSquare gamma (KindArrow a b) =
  case getSquare gamma a of
    Just SquareSquare -> case getSquare gamma b of
                           Just SquareSquare -> Just SquareSquare
                           _ -> Nothing
    _ -> Nothing


{-
(weak) (s = square)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin Gamma
    \Gamma, x : C |- A : B
-}
getSquare (TypeDeclaration (x, c) : gamma) a =
  if x `notElem` (getDomain gamma)
  then do
    b <- getSquare gamma a
    case getSquare gamma c of
      Just SquareSquare -> return b
      _ -> Nothing
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin Gamma
    \Gamma, x : C |- A : B
-}
getSquare (TermDeclaration (x, c) : gamma) a =
  if x `notElem` (getDomain gamma)
  then do
    b <- getSquare gamma a
    case getKind gamma c of
      Just KindStar -> return b
      _ -> Nothing
  else Nothing


-- getKind

getKind :: Context -> Type -> Maybe Kind

{-
(var) (s = square)
   \Gamma |- A : s
----------------------  if x \notin \Gamma
\Gamma, x : A |- x : A
-}
getKind (TypeDeclaration (x', a) : gamma) (TypeVar x) =
  if (x' == x) && (x `notElem` (getDomain gamma))
  then
    case getSquare gamma a of
      Just SquareSquare -> return a
      _ -> Nothing
  else Nothing

getKind [] (TypeVar _) = Nothing

{-
\alpha -> \sigma : *
\beta -> (\sigma -> \alpha) : *

(form) (s = star)
\Gamma |- A : s  \Gamma |- B : s
--------------------------------
     \Gamma |- A -> B : s
-}
getKind gamma (TypeArrow a b) =
  case getKind gamma a of
    Just KindStar -> case getKind gamma b of
                       Just KindStar -> Just KindStar
                       _ -> Nothing
    _ -> Nothing

{-
(appl) (type)
\Gamma |- M : A -> B  \Gamma |- N : A
-------------------------------------
            \Gamma |- M N : B
-}
getKind gamma (TypeApp m n) = do
  ki_m <- getKind gamma m
  ki_n <- getKind gamma n
  case ki_m of
    KindArrow a b -> if ki_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = square)
\Gamma, x : A |- M : B  \Gamma |- A -> B : s
--------------------------------------------
    \Gamma |- \lambda x : A . M : A -> B
-}
getKind gamma (TypeAbs x a m) =
  let gamma' = TypeDeclaration (x, a) : gamma in do
    b <- getKind gamma' m
    case getSquare gamma (KindArrow a b) of
      Just SquareSquare -> return (KindArrow a b)
      _ -> Nothing


{-
(weak) (s = square)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin Gamma
    \Gamma, x : C |- A : B
-}
getKind (TypeDeclaration (x, c) : gamma) a =
  if x `notElem` (getDomain gamma)
  then do
    b <- getKind gamma a
    case getSquare gamma c of
      Just SquareSquare -> return b
      _ -> Nothing
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin Gamma
    \Gamma, x : C |- A : B
-}
getKind (TermDeclaration (x, c) : gamma) a =
  if x `notElem` (getDomain gamma)
  then do
    b <- getKind gamma a
    case getKind gamma c of
      Just KindStar -> return b
      _ -> Nothing
  else Nothing


-- getType

getType :: Context -> Term -> Maybe Type

{-
(var) (s = star)
   \Gamma |- A : s
----------------------  if x \notin \Gamma
\Gamma, x : A |- x : A
-}
getType (TermDeclaration (x', a) : gamma) (TermVar x) =
  if (x' == x) && (x `notElem` (getDomain gamma))
  then
    case getKind gamma a of
      Just KindStar -> return a
      _ -> Nothing
  else Nothing

getType [] (TermVar _) = Nothing

{-
(appl) (term)
\Gamma |- M : A -> B  \Gamma |- N : A
-------------------------------------
            \Gamma |- M N : B
-}
getType gamma (TermApp m n) = do
  ty_m <- getType gamma m
  ty_n <- getType gamma n
  case ty_m of
    TypeArrow a b -> if ty_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = star)
\Gamma, x : A |- M : B  \Gamma |- A -> B : s
--------------------------------------------
    \Gamma |- \lambda x : A . M : A -> B
-}
getType gamma (TermAbs x a m) =
  let gamma' = TermDeclaration (x, a) : gamma in do
    b <- getType gamma' m
    case getKind gamma (TypeArrow a b) of
      Just KindStar -> return (TypeArrow a b)
      _ -> Nothing


{-
(weak) (s = square)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin Gamma
    \Gamma, x : C |- A : B
-}
getType (TypeDeclaration (x, c) : gamma) a =
  if x `notElem` (getDomain gamma)
  then do
    b <- getType gamma a
    case getSquare gamma c of
      Just SquareSquare -> return b
      _ -> Nothing
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin Gamma
    \Gamma, x : C |- A : B
-}
getType (TermDeclaration (x, c) : gamma) a =
  if x `notElem` (getDomain gamma)
  then do
    b <- getType gamma a
    case getKind gamma c of
      Just KindStar -> return b
      _ -> Nothing
  else Nothing

[Mario Carneiro]

Patrick Thomas said:

How do you deal with the weakening rule when writing a type checker for λω_ (STLC + higher-kinded type operators) when it seems that its conclusion can mirror the conclusion of other rules?

Generally typecheckers don't ever weaken; they only use a variant on the hypothesis rule that says that Gamma |- x : T when (x: T) \in Gamma

[Patrick Thomas]

How do they ensure that the types in the declarations in the context are permissible?

[Patrick Thomas]

Do I add a function that iterates through the context checking that each type below square has been previously declared in the context?

[Patrick Thomas]

Do you know where I might find existing implementations in Haskell of the type checkers for the eight corners of the lambda cube?

[Patrick Thomas]

Am I taking the wrong approach?

[Patrick Thomas]

Mario Carneiro said:

Patrick Thomas said:

How do you deal with the weakening rule when writing a type checker for λω_ (STLC + higher-kinded type operators) when it seems that its conclusion can mirror the conclusion of other rules?

Generally typecheckers don't ever weaken; they only use a variant on the hypothesis rule that says that Gamma |- x : T when (x: T) \in Gamma

@Mario Carneiro My text has:

 It becomes also clear from this example that the (var) -rule introduced in the present chapter is
less general than the one in e. g. the system λ→ (see Definition 2.4.5), since the present (var) -rule
only allows the derivation of the newly added, final declaration x: A of the context. See lines (2)
and (3) in the derivation. In λ→, however, any declaration x: σ occurring in Γ, is derivable with
respect to this Γ. It is a natural desire that we can do as much in our present system λω as
in λ→. So, for example, we want to be able to derive not only α: ∗, x: α ⊢ x: α, but
also: (?1) α: ∗, x: α ⊢ α: ∗, which is impossible with the present rules.
...
 The solution to the previously explained problem is the addition of a new rule. This rule, called
Weakening, allows us to ‘weaken’ the context of a judgement by adding new declarations, provided
that the ‘types’ of the new declarations are ‘well-formed’.

The derivation rules they give are:

Screenshot-from-2021-07-12-19-44-56.png

Are there a different set of rules that are more canonical for this system?

[Mario Carneiro]

That's fine for the abstract presentation; what I'm saying is that in practice typecheckers defer all uses of the (weak) rule to immediately before an application of (var), so that you get the combined (var+weak) rule that I described

[Mario Carneiro]

Similarly, you would use a (sort+weak) rule of the form Gamma |- * : box

[Patrick Thomas]

How do they ensure that the types in the context are permissible?

[Mario Carneiro]

you check that when you first construct the context

[Mario Carneiro]

that is, in the (abst) rule

[Mario Carneiro]

you could also check it in every application of the (var+weak) and (sort+weak) rules, but that's a lot more expensive

[Patrick Thomas]

Do we only usually give an empty context in the first call to getType?

[Mario Carneiro]

presumably

[Mario Carneiro]

alternatively it can be a context that you have pre-checked

[Mario Carneiro]

or one that was previously constructed somehow and you have the invariant that it is checked

[Patrick Thomas]

Do you lose anything by that requirement (that the initial context is empty)?

[Patrick Thomas]

I guess you can just add on more abstractions?

[Mario Carneiro]

It's just reversing the "polarity" of the context: in Gamma |- e : T, we are assuming that Gamma is type correct and proving that e is type correct (whether T is an input or output depends on the context, but it's usually an output), rather than proving that both Gamma and e are type correct (which is what your given rules are doing)

[Mario Carneiro]

With Gamma as an input, it means that we can have rules like Gamma |- * : box and Gamma, x : T |- x : T with no hypotheses

[Mario Carneiro]

but the lambda rule has an extra hypothesis: Gamma |- A : s and Gamma, x : A |- M : B implies Gamma |- (\lam x : A. M) : A -> B

[Mario Carneiro]

So we aren't requiring that the initial context is empty, only that the initial context is type correct

[Mario Carneiro]

of course the empty context is type correct so that's an easy way to start out

[Mario Carneiro]

If you want to explicitly type check a context you can use a judgment Γ ⊢ defined like this:

       Γ ⊢   Γ ⊢ T : s   x ∉ Dom(Γ)
---    ----------------------------
∅ ⊢            Γ, x : T ⊢

[Patrick Thomas]

I'll give that a try. Thank you!

[Patrick Thomas]

Do we need to step out of these rules to check T : s or just check that T is a type or a kind?

[Mario Carneiro]

The way I've just presented it, Gamma |- e : T implies Gamma |- T : s (or possibly also |- T : s if you don't have dependent types), so you don't need to check it in most cases

[Mario Carneiro]

This is why the lambda rule I gave doesn't need to also assume Gamma |- B : s

[Patrick Thomas]

I'm sorry, I'm not sure I understand why that first implication holds.

[Patrick Thomas]

Because we are assuming gamma is type correct?

[Mario Carneiro]

We just make sure it holds for all the rules

[Mario Carneiro]

We do need to assume gamma is type correct though, since for it to work in the (var) rule Gamma, x : T |- x : T (which has no assumptions), we need Gamma, x : T |- to supply the needed Gamma |- T : s assertion

[Mario Carneiro]

That is, I claim one can prove:

Gamma |- and Gamma |- e : T implies Gamma |- T : s
Proof: By induction on Gamma |- e : T.

[Mario Carneiro]

Actually, looking again at the (abst) rule, I think you need to assume Gamma |- B : s because otherwise you could typecheck |- (λ T : s. λ x : T. x) : s -> T -> T which would be bad because T has escaped its scope

[Patrick Thomas]

Do the rules from the screenshot work (other than the weakening)?

[Mario Carneiro]

I guess s is a metavariable for * or box? If so, then yes. They are using the shorthand Gamma |- A -> B : s which is equivalent to the conjunction Gamma |- A : s and Gamma |- B : s

[Patrick Thomas]

Yes, sorry, s is a metavariable for * or box.

[Mario Carneiro]

Ah, I guess those rules do not satisfy the theorem I claimed, because Gamma |- box : ? does not typecheck

[Mario Carneiro]

In lean you have an infinite hierarchy of universes so that everything on the right of a type judgment can also appear on the left

[Patrick Thomas]

No, I don't think that is the case here. box is as high as it goes.

[Mario Carneiro]

You can still repair the theorem to say that Gamma |- e : T implies Gamma |- T : s or T = box

[Mario Carneiro]

The book version also has Gamma |- e : T implies Gamma |-, while my version has the weaker theorem Gamma |- and Gamma |- e : T implies Gamma |- T : s or T = box

[Patrick Thomas]

Where in the book?

[Mario Carneiro]

Oh I don't know, I don't know your book. I'm just saying that you could prove that theorem about those rules

[Mario Carneiro]

it's pretty straightforward by induction on Gamma |- e : T

[Patrick Thomas]

Your version is the book's set of rules minus (weak), but plus the two context rules?

[Patrick Thomas]

I'm guessing it is not possible to create a type checker using just the book's rules as is?

[Mario Carneiro]

It's possible to write a type checker using weak nondeterministically (and sometimes it is necessary, if the type theory is complicated enough), but it's a lot harder, you have to do backtracking

[Mario Carneiro]

It's also possible to defer all uses of (weak) without changing the (sort) and (var) rules, that just means checking Gamma |- at all the leaves of the type derivation

[Patrick Thomas]

What do you mean by defer? Just to be sure, what does Gamma |- mean precisely?

[Patrick Thomas]

Do you mean call (weak) every time it would otherwise return Nothing?

[Mario Carneiro]

Just to be sure, what does Gamma |- mean precisely?

Mario Carneiro said:

If you want to explicitly type check a context you can use a judgment Γ ⊢ defined like this:

       Γ ⊢   Γ ⊢ T : s   x ∉ Dom(Γ)
---    ----------------------------
∅ ⊢            Γ, x : T ⊢

[Mario Carneiro]

What do you mean by defer?

I mean to never use the (weak) rule unless no other rule applies. That means when typechecking a lambda, arrow, or application you never use (weak) even though it could be used; the only time you use it is when the goal is e.g. x : A, y : B |- x : A in which case the (var) rule does not directly apply because the variable is not the last one in the list, so you have to use (weak) first and then (var); or with x : A |- * : box you can't apply (sort) because the context is not empty so you have to apply (weak) until the context is empty, and then (sort). These combinations of weak and then var/sort are what I was calling (var+weak) and (sort+weak), and they are basically derived rules that look like this:

• (sort+weak): Gamma |- * : box
• (var+weak): Gamma |- x : A if (x : A) \in Gamma

[Mario Carneiro]

In general, you can't just choose not to use a certain rule when it could apply, because you might falsely reject a well typed expression, but in this case it is admissible because weak "commutes" with the other rules: a proof by (weak) followed by (appl) can be transformed into a proof by (appl) with (weak) in both subgoals. By performing such commutations we push all uses of (weak) to the leaves (var) and (sort), resulting in the aforementioned combined rules

[Mario Carneiro]

More formally, one can prove that if Γ |- e : T in the original system with (weak), then for every Γ' >= Γ (where Γ <= Γ' means that Γ is a sublist of Γ', i.e. some bindings are removed but the order is preserved), Γ' |- e : T in the system without (weak) and with the (var+weak) and (sort+weak) rules.

The proof is by induction on Γ |- e : T (assume in each case that Γ' >= Γ is given):

• If (weak) is used to derive Γ, x : A |- e : T from Γ |- e : T, then Γ' >= (Γ, x : A) implies Γ' >= Γ so Γ' |- e : T by the IH.
• If (var) is used to derive Γ, x : A |- x : A, then Γ' >= (Γ, x : A) implies (x : A) \in Γ' so Γ' |- x : A by the (var+weak) rule.
• If (sort) is used to derive |- * : box, then Γ' |- * : boxby the (sort+weak) rule.
• If (appl) is used to derive Γ |- M N : B from Γ |- M : A -> B and Γ |- N : A, then Γ' |- M : A -> B and Γ' |- N : A by the IH so (appl) applies. (The (form) and (conv) rules are similar.)
• If (abst) is used to derive Γ |- (λ x: A. M) : A -> B from Γ |- A -> B : s and Γ, x : A |- M : B, then by the IH Γ' |- A -> B : s, and Γ' >= Γ implies (Γ', x : A) >= (Γ, x : A) (here it is important that we have a sublist relation, not just an initial segment) so Γ', x : A |- M : B by the IH, so (abst) applies.

[Patrick Thomas]

The (var + weak) rule you have above is less restrictive than just using weak only when the var rule does not apply right? I think that, because I tried the code below, which I think is what you meant by using weak only when the var rule does not apply (?) and it doesn't type check getSquare [(TypeDeclaration ("a", KindStar)), (TermDeclaration ("x", (TypeVar "a")))] KindStar

data Square = SquareSquare
  deriving (Show, Eq)

data Kind = KindStar
          | KindArrow Kind Kind
            deriving (Show, Eq)

data Type = TypeVar String           -- V
          | TypeArrow Type Type      -- Type -> Type
          | TypeApp Type Type        -- Type Type
          | TypeAbs String Kind Type -- \lambda V : Kind . Type
            deriving (Show, Eq)

data Term = TermVar String           -- V'
          | TermApp Term Term        -- Term Term
          | TermAbs String Type Term -- \lambda V' : Type . Term
            deriving (Show, Eq)


data Declaration = TermDeclaration (String, Type)
                 | TypeDeclaration (String, Kind)

type Context = [Declaration]

getDomain :: Context -> [String]
getDomain []                                   = []
getDomain (TermDeclaration (x, _) : gamma)     = x : (getDomain gamma)
getDomain (TypeDeclaration (alpha, _) : gamma) = alpha : (getDomain gamma)


-- getSquare

getSquare :: Context -> Kind -> Maybe Square

{-
(sort)
\empty |- * : Square
-}
getSquare [] KindStar = Just SquareSquare


{-
(weak) (s = square)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
\Gamma, x : C |- A : B
-}
getSquare (TypeDeclaration (x, c) : gamma) KindStar =
  if x `notElem` (getDomain gamma)
  then
    case getSquare gamma c of
      Just SquareSquare -> (getSquare gamma KindStar)
      _ -> Nothing
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
\Gamma, x : C |- A : B
-}
getSquare (TermDeclaration (x, c) : gamma) KindStar =
  if x `notElem` (getDomain gamma)
  then
    case getKind gamma c of
      Just KindStar -> (getSquare gamma KindStar)
      _ -> Nothing
  else Nothing


{-
* -> * : Square
* -> (* -> *) : Square

(form) (s = square)
\Gamma |- A : s  \Gamma |- B : s
--------------------------------
     \Gamma |- A -> B : s
-}
getSquare gamma (KindArrow a b) =
  case getSquare gamma a of
    Just SquareSquare -> case getSquare gamma b of
                           Just SquareSquare -> Just SquareSquare
                           _ -> Nothing
    _ -> Nothing


-- getKind

getKind :: Context -> Type -> Maybe Kind

{-
(var) (s = square)
   \Gamma |- C : s
----------------------  if x \notin \Gamma
\Gamma, x : C |- x : C
-}

{-
(weak) (s = square)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
\Gamma, x : C |- A : B
-}

getKind (TypeDeclaration (x, c) : gamma) (TypeVar x') =
  if x `notElem` (getDomain gamma)
  then
    if x == x'
    then
      case getSquare gamma c of
        Just SquareSquare -> return c
        _ -> Nothing
    else
      case getSquare gamma c of
        Just SquareSquare -> getKind gamma (TypeVar x')
        _ -> Nothing
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
\Gamma, x : C |- A : B
-}
getKind (TermDeclaration (x, c) : gamma) (TypeVar a) =
  if x `notElem` (getDomain gamma)
  then
    case getKind gamma c of
      Just KindStar -> getKind gamma (TypeVar a)
      _ -> Nothing
  else Nothing

getKind [] (TypeVar _) = Nothing


{-
\alpha -> \sigma : *
\beta -> (\sigma -> \alpha) : *

(form) (s = star)
\Gamma |- A : s  \Gamma |- B : s
--------------------------------
     \Gamma |- A -> B : s
-}
getKind gamma (TypeArrow a b) =
  case getKind gamma a of
    Just KindStar -> case getKind gamma b of
                       Just KindStar -> Just KindStar
                       _ -> Nothing
    _ -> Nothing

{-
(appl) (type)
\Gamma |- M : A -> B  \Gamma |- N : A
-------------------------------------
            \Gamma |- M N : B
-}
getKind gamma (TypeApp m n) = do
  ki_m <- getKind gamma m
  ki_n <- getKind gamma n
  case ki_m of
    KindArrow a b -> if ki_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = square)
\Gamma, x : A |- M : B  \Gamma |- A -> B : s
--------------------------------------------
    \Gamma |- \lambda x : A . M : A -> B
-}
getKind gamma (TypeAbs x a m) =
  let gamma' = TypeDeclaration (x, a) : gamma in do
    b <- getKind gamma' m
    case getSquare gamma (KindArrow a b) of
      Just SquareSquare -> return (KindArrow a b)
      _ -> Nothing


-- getType

getType :: Context -> Term -> Maybe Type

{-
(var) (s = square)
   \Gamma |- C : s
----------------------  if x \notin \Gamma
\Gamma, x : C |- x : C
-}

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
\Gamma, x : C |- A : B
-}

getType (TermDeclaration (x, c) : gamma) (TermVar x') =
  if x `notElem` (getDomain gamma)
  then
    if x == x'
    then
      case getKind gamma c of
        Just KindStar -> return c
        _ -> Nothing
    else
      case getKind gamma c of
        Just KindStar -> getType gamma (TermVar x')
        _ -> Nothing
  else Nothing

{-
(weak) (s = square)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
\Gamma, x : C |- A : B
-}
getType (TypeDeclaration (x, c) : gamma) (TermVar a) =
  if x `notElem` (getDomain gamma)
  then
    case getSquare gamma c of
      Just SquareSquare -> getType gamma (TermVar a)
      _ -> Nothing
  else Nothing

getType [] (TermVar _) = Nothing


{-
(appl) (term)
\Gamma |- M : A -> B  \Gamma |- N : A
-------------------------------------
            \Gamma |- M N : B
-}
getType gamma (TermApp m n) = do
  ty_m <- getType gamma m
  ty_n <- getType gamma n
  case ty_m of
    TypeArrow a b -> if ty_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = star)
\Gamma, x : A |- M : B  \Gamma |- A -> B : s
--------------------------------------------
    \Gamma |- \lambda x : A . M : A -> B
-}
getType gamma (TermAbs x a m) =
  let gamma' = TermDeclaration (x, a) : gamma in do
    b <- getType gamma' m
    case getKind gamma (TypeArrow a b) of
      Just KindStar -> return (TypeArrow a b)
      _ -> Nothing

[Patrick Thomas]

Basically, the weakening rule pulls off the type declaration and then tries to find the type of "a" in the term declaration, which it can't any more, because it lost it when the type declaration was pulled off. At least that is what I think is happening.

[Patrick Thomas]

Or maybe that shouldn't actually be typeable?

[Patrick Thomas]

I think at least that everything that is typeable in this code is typeable in the rules from the text? I'm not sure about the other way around?

[Mario Carneiro]

I think the issue is that you have the type context backwards

[Mario Carneiro]

Haskell lists are destructured from the front, so you want the deepest bindings on the left

[Mario Carneiro]

hopefully you can confirm that

getSquare [(TermDeclaration ("x", (TypeVar "a"))), (TypeDeclaration ("a", KindStar))] KindStar = Just SquareSquare

[Patrick Thomas]

Yep.

*Main> getSquare [(TermDeclaration ("x", (TypeVar "a"))), (TypeDeclaration ("a", KindStar))] KindStar
Just SquareSquare

[Patrick Thomas]

I was expecting it should type check both ways, but I guess it shouldn't?

[Patrick Thomas]

Each item you pull off the end of the context should type check in the remaining context?

[Mario Carneiro]

yes

[Mario Carneiro]

if you need the variable to typecheck in its own context, you will get into circularities

[Patrick Thomas]

That makes sense.

[Patrick Thomas]

Thank you!

[Patrick Thomas]

I cleaned my code up and added some examples.

-- "Type Theory and Formal Proof" by Rob Nederpelt and Herman Geuvers
-- lambda underline omega (types dependent on types)


data Box = BoxBox
  deriving (Show, Eq)

data Kind = KindStar
          | KindArrow Kind Kind      -- Kind -> Kind
            deriving (Show, Eq)

data Type = TypeVar String           -- V
          | TypeArrow Type Type      -- Type -> Type
          | TypeApp Type Type        -- Type Type
          | TypeAbs String Kind Type -- \lambda V : Kind . Type
            deriving (Show, Eq)

data Term = TermVar String           -- V'
          | TermApp Term Term        -- Term Term
          | TermAbs String Type Term -- \lambda V' : Type . Term
            deriving (Show, Eq)


data Declaration = TermDeclaration (String, Type)
                 | TypeDeclaration (String, Kind)

type Context = [Declaration]

getDomain :: Context -> [String]
getDomain []                                   = []
getDomain (TermDeclaration (x, _) : gamma)     = x : (getDomain gamma)
getDomain (TypeDeclaration (alpha, _) : gamma) = alpha : (getDomain gamma)


-- getBox

getBox :: Context -> Kind -> Maybe Box

{-
(sort)
\empty |- * : Box
-}
getBox [] KindStar = return BoxBox

{-
(weak) (s = box) (A = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getBox (TypeDeclaration (x, c) : gamma) KindStar =
  let a = KindStar in do
    b <- getBox gamma a
    s <- getBox gamma c
    if s == BoxBox && x `notElem` (getDomain gamma)
    then return b
    else Nothing

{-
(weak) (s = star) (A = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getBox (TermDeclaration (x, c) : gamma) KindStar =
  let a = KindStar in do
    b <- getBox gamma a
    s <- getKind gamma c
    if s == KindStar && x `notElem` (getDomain gamma)
    then return b
    else Nothing

{-
* -> * : Box
* -> (* -> *) : Box

(form) (s = box)
\Gamma |- A : s  \Gamma |- B : s
--------------------------------
      \Gamma |- A -> B : s
-}
getBox gamma (KindArrow a b) =
  let s = BoxBox in do
    s1 <- getBox gamma a
    s2 <- getBox gamma b
    if s1 == s && s2 == s then return s else Nothing


-- getKind

getKind :: Context -> Type -> Maybe Kind

{-
(var) (s = box)
   \Gamma |- C : s
----------------------  if x \notin \Gamma
\Gamma, x : C |- x : C
-}

{-
(weak) (s = box)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}

{-
If x == x' then the var rule applies and it is used.
If x != x' then the var rule does not apply and the weak rule is used instead.
-}

getKind (TypeDeclaration (x, c) : gamma) (TypeVar x') = do
  s <- getBox gamma c
  if s == BoxBox && x `notElem` (getDomain gamma) then
    if x == x' then return c else getKind gamma (TypeVar x')
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getKind (TermDeclaration (x, c) : gamma) (TypeVar x') = do
  s <- getKind gamma c
  if s == KindStar && x `notElem` (getDomain gamma)
  then getKind gamma (TypeVar x')
  else Nothing

getKind [] (TypeVar _) = Nothing


{-
\alpha -> \sigma : *
\beta -> (\sigma -> \alpha) : *

(form) (s = star)
\Gamma |- A : s  \Gamma |- B : s
--------------------------------
      \Gamma |- A -> B : s
-}
getKind gamma (TypeArrow a b) =
  let s = KindStar in do
    s1 <- getKind gamma a
    s2 <- getKind gamma b
    if s1 == s && s2 == s then return s else Nothing

{-
(appl) (type)
\Gamma |- M : A -> B  \Gamma |- N : A
-------------------------------------
          \Gamma |- M N : B
-}
getKind gamma (TypeApp m n) = do
  ki_m <- getKind gamma m
  ki_n <- getKind gamma n
  case ki_m of
    KindArrow a b -> if ki_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = box)
\Gamma, x : A |- M : B  \Gamma |- A -> B : s
--------------------------------------------
    \Gamma |- \lambda x : A . M : A -> B
-}
getKind gamma (TypeAbs x a m) =
  let gamma' = TypeDeclaration (x, a) : gamma in do
    b <- getKind gamma' m
    s <- getBox gamma (KindArrow a b)
    if s == BoxBox then return (KindArrow a b) else Nothing


-- getType

getType :: Context -> Term -> Maybe Type

{-
(var) (s = box)
   \Gamma |- C : s
----------------------  if x \notin \Gamma
\Gamma, x : C |- x : C
-}

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}

{-
If x == x' then the var rule applies and it is used.
If x != x' then the var rule does not apply and the weak rule is used instead.
-}

getType (TermDeclaration (x, c) : gamma) (TermVar x') = do
  s <- getKind gamma c
  if s == KindStar && x `notElem` (getDomain gamma) then
    if x == x' then return c else getType gamma (TermVar x')
  else Nothing

{-
(weak) (s = box)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getType (TypeDeclaration (x, c) : gamma) (TermVar x') = do
  s <- getBox gamma c
  if s == BoxBox && x `notElem` (getDomain gamma)
  then getType gamma (TermVar x')
  else Nothing

getType [] (TermVar _) = Nothing


{-
(appl) (term)
\Gamma |- M : A -> B  \Gamma |- N : A
-------------------------------------
          \Gamma |- M N : B
-}
getType gamma (TermApp m n) = do
  ty_m <- getType gamma m
  ty_n <- getType gamma n
  case ty_m of
    TypeArrow a b -> if ty_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = star)
\Gamma, x : A |- M : B  \Gamma |- A -> B : s
--------------------------------------------
    \Gamma |- \lambda x : A . M : A -> B
-}
getType gamma (TermAbs x a m) =
  let gamma' = TermDeclaration (x, a) : gamma in do
    b <- getType gamma' m
    s <- getKind gamma (TypeArrow a b)
    if s == KindStar then return (TypeArrow a b) else Nothing


{-
Examples:

*Main> getKind [] (TypeAbs "a" KindStar (TypeArrow (TypeVar "a") (TypeVar "a")))
Just (KindArrow KindStar KindStar)

*Main> getKind [] (TypeAbs "a" KindStar (TypeAbs "b" KindStar (TypeArrow (TypeVar "a") (TypeVar "b"))))
Just (KindArrow KindStar (KindArrow KindStar KindStar))

*Main> getKind [] (TypeAbs "a" (KindArrow KindStar KindStar) (TypeVar "a"))
Just (KindArrow (KindArrow KindStar KindStar) (KindArrow KindStar KindStar))

*Main> getType [(TermDeclaration ("x", (TypeVar "a"))), (TypeDeclaration ("a", KindStar))] (TermVar "x")
Just (TypeVar "a")

*Main> getKind [(TermDeclaration ("x", (TypeVar "a"))), (TypeDeclaration ("a", KindStar))] (TypeVar "a")
Just KindStar

*Main> getKind [(TypeDeclaration ("b", KindStar)), (TypeDeclaration ("a", KindStar))] (TypeVar "a")
Just KindStar

*Main> getKind [(TypeDeclaration ("b", KindStar)), (TypeDeclaration ("a", KindStar))] (TypeVar "b")
Just KindStar

*Main> getBox [(TypeDeclaration ("a", KindStar))] KindStar
Just BoxBox

*Main> getBox [(TypeDeclaration ("a", KindStar))] (KindArrow KindStar KindStar)
Just BoxBox

*Main> getKind [(TypeDeclaration ("b", KindStar))] (TypeApp (TypeAbs "a" KindStar (TypeArrow (TypeVar "a") (TypeVar "a"))) (TypeVar "b"))
Just KindStar
-}

[Patrick Thomas]

Is this the correct syntax for λP?

data Box = BoxBox
           deriving (Show, Eq)

data Kind = KindStar
          | KindApp Kind Term         -- Kind Term
          | KindAbs String Type Kind  -- \Pi V' : Type . Kind
            deriving (Show, Eq)

data Type = TypeVar String            -- V
          | TypeApp Type Term         -- Type Term
          | TypeAbs String Type Type  -- \Pi V' : Type . Type
            deriving (Show, Eq)

data Term = TermVar String            -- V'
          | TermApp Term Term         -- Term Term
          | TermAbs String Type Term  -- \lambda V' : Type . Term
            deriving (Show, Eq)

[Mario Carneiro]

I don't recall KindAbs being a thing. Also it doesn't match up with KindApp, so I don't know what beta reduction at that level would look like

[Mario Carneiro]

From the description on wikipedia it looks like there aren't any kinds other than star

[Patrick Thomas]

I'm confused about that too. I'm trying to figure it out from this: Screenshot-from-2021-07-21-21-35-21.png

[Patrick Thomas]

s is either KindStar or BoxBox as before.

[Mario Carneiro]

There is another source here: http://ceur-ws.org/Vol-878/paper2.pdf (ignore the modulo part)

[Mario Carneiro]

your variables shouldn't have to range over different types

[Mario Carneiro]

What is that screenshot from?

[Patrick Thomas]

"Type Theory and Formal Proof" by Rob Nederpelt and Herman Geuvers. I have an electronic version I bought on ebooks.com.

[Mario Carneiro]

The rule compression in that picture is convenient for presentation, but it's much clearer to just separate them all out, because there are two copies of everything and this makes it clearer what is what.

(sort) |- * kind
(Var) K kind => t :: K |- t :: K
(var) A : * => x : A |- x : A
(Form) A : * => x : A |- K kind => ΠΠ x: A. K kind
(form) A : * => x : A |- B :: * => Π x: A. B :: *
(Appl) F :: ΠΠ x: A. K => N : A => F @ N :: K[x:=N]
(appl) M : Π x: A. B => N : A => M N : B[x:=N]
(Abst) x : A |- T :: K => ΠΠ x: A. K kind => Λ x: A. T :: ΠΠ x: A. K
(abst) x : A |- M : B => Π x: A. B : * => λ x: A. M : Π x: A. B

[Patrick Thomas]

I had forgotten about the first answer to this question: https://cstheory.stackexchange.com/questions/36054/how-do-you-get-the-calculus-of-constructions-from-the-other-points-in-the-lambda
Maybe?:

data Box = BoxBox
           deriving (Show, Eq)

data Kind = KindStar
          | KindPi String Type Kind  -- \Pi V' : Type . Kind
            deriving (Show, Eq)

data Type = TypeVar String            -- V
          | TypeApp Type Term         -- Type Term
          | TypePi String Type Type  -- \Pi V' : Type . Type
          | TypeAbs String Type Type -- /\  V' : Type . Type
            deriving (Show, Eq)

data Term = TermVar String            -- V'
          | TermApp Term Term         -- Term Term
          | TermAbs String Type Term  -- \lambda V' : Type . Term
            deriving (Show, Eq)

[Mario Carneiro]

Pi is not "Abs", that means abstraction aka lambda

[Patrick Thomas]

I see.

[Mario Carneiro]

• There are three versions of the typing judgment: M : A, T :: K and K kind (which the book writes K : box, but box isn't really a term so this is mostly just to keep up the colon style)

• There are two pi-like types: Π x: A. B produces a type and ΠΠ x: A. K produces a kind. Note that the variable is always a x: A binder, no t :: K binders exist in this language.
  There are two applications: F @ N where F is a type constructor and N is a term, and M N where M and N are terms.

• There are two lambda-like terms: Λ x: A. T produces a type where T is a type, and λ x: A. M produces a term where M is a term.

• There are also two substitutions: both types and terms can have term variables substituted into them, used in the (Appl) and (appl) rules.

[Mario Carneiro]

Your haskell looks right

[Patrick Thomas]

Thank you!

[Mario Carneiro]

(although you don't need Box as I mentioned)

[Patrick Thomas]

@Mario Carneiro If you have time at some point, would you mind checking if I did this right? I'm most uncertain about whether I handled the substitution in the apply rules correctly. I have ignored alpha equivalence for the time being.

-- "Type Theory and Formal Proof" by Rob Nederpelt and Herman Geuvers
-- lambda P (types dependent on terms)

import Data.Set


data Box = BoxBox
           deriving (Show, Eq)

data Kind = KindStar
          | KindPi String Type Kind  -- \Pi V' : Type . Kind
            deriving (Show, Eq)

data Type = TypeVar String           -- V
          | TypeApp Type Term        -- Type Term
          | TypePi String Type Type  -- \Pi V' : Type . Type
          | TypeAbs String Type Type -- /\  V' : Type . Type
            deriving (Show, Eq)

data Term = TermVar String           -- V'
          | TermApp Term Term        -- Term Term
          | TermAbs String Type Term -- \lambda V' : Type . Term
            deriving (Show, Eq)


getFreeTermVariableSetInType :: Type -> Data.Set.Set String
getFreeTermVariableSetInType (TypeVar _) = Data.Set.empty
getFreeTermVariableSetInType (TypeApp m n) =
  Data.Set.union (getFreeTermVariableSetInType m) (getFreeTermVariableSetInTerm n)
getFreeTermVariableSetInType (TypePi x _ n) =
  Data.Set.difference (getFreeTermVariableSetInType n) (Data.Set.singleton x)
getFreeTermVariableSetInType (TypeAbs x _ n) =
  Data.Set.difference (getFreeTermVariableSetInType n) (Data.Set.singleton x)

getFreeTermVariableSetInTerm :: Term -> Data.Set.Set String
getFreeTermVariableSetInTerm (TermVar x) = Data.Set.singleton x
getFreeTermVariableSetInTerm (TermApp m n) =
  Data.Set.union (getFreeTermVariableSetInTerm m) (getFreeTermVariableSetInTerm n)
getFreeTermVariableSetInTerm (TermAbs x _ n) =
  Data.Set.difference (getFreeTermVariableSetInTerm n) (Data.Set.singleton x)


-- substituteInType m x n = m [ x := n ]
substituteInType :: Type -> String -> Term -> Type
substituteInType e@(TypeVar _) _ _ = e
substituteInType (TypeApp p q) x n = TypeApp (substituteInType p x n) (substituteInTerm q x n)
substituteInType e@(TypePi y q p) x n
  | x == y = e
  | x /= y && x `Data.Set.notMember` (getFreeTermVariableSetInType e) = e
  | x /= y && y `Data.Set.notMember` (getFreeTermVariableSetInTerm n) =
      TypePi y q (substituteInType p x n)
  | otherwise = error "bad input"
substituteInType e@(TypeAbs y q p) x n
  | x == y = e
  | x /= y && x `Data.Set.notMember` (getFreeTermVariableSetInType e) = e
  | x /= y && y `Data.Set.notMember` (getFreeTermVariableSetInTerm n) =
      TypeAbs y q (substituteInType p x n)
  | otherwise = error "bad input"

-- substituteInTerm m x n = m [ x := n ]
substituteInTerm :: Term -> String -> Term -> Term
substituteInTerm e@(TermVar y) x n = if x == y then n else e
substituteInTerm (TermApp p q) x n = TermApp (substituteInTerm p x n) (substituteInTerm q x n)
substituteInTerm e@(TermAbs y q p) x n
  | x == y = e
  | x /= y && x `Data.Set.notMember` (getFreeTermVariableSetInTerm e) = e
  | x /= y && y `Data.Set.notMember` (getFreeTermVariableSetInTerm n) =
      TermAbs y q (substituteInTerm p x n)
  | otherwise = error "bad input"


data Declaration = TermDeclaration (String, Type)
                 | TypeDeclaration (String, Kind)

type Context = [Declaration]

getDomain :: Context -> [String]
getDomain []                                   = []
getDomain (TermDeclaration (x, _) : gamma)     = x : (getDomain gamma)
getDomain (TypeDeclaration (alpha, _) : gamma) = alpha : (getDomain gamma)


-- getBox

getBox :: Context -> Kind -> Maybe Box

{-
(sort)
\empty |- * : Box
-}
getBox [] KindStar = return BoxBox

{-
(weak) (s = box) (A = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getBox (TypeDeclaration (x, c) : gamma) KindStar =
  let a = KindStar in do
    b <- getBox gamma a
    s <- getBox gamma c
    if s == BoxBox && x `notElem` (getDomain gamma)
    then return b
    else Nothing

{-
(weak) (s = star) (A = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getBox (TermDeclaration (x, c) : gamma) KindStar =
  let a = KindStar in do
    b <- getBox gamma a
    s <- getKind gamma c
    if s == KindStar && x `notElem` (getDomain gamma)
    then return b
    else Nothing

{-
(form) (s = box)
\Gamma |- A : *  \Gamma, x : A |- B : s
---------------------------------------
      \Gamma |- Pi x : A . B : s
-}
getBox gamma (KindPi x a b) = -- a = Type, b = Kind
  let gamma' = TermDeclaration (x, a) : gamma in do
    ki_a <- getKind gamma a
    s <- getBox gamma' b
    if ki_a == KindStar && s == BoxBox then return s else Nothing


-- getKind

getKind :: Context -> Type -> Maybe Kind

{-
(var) (s = box)
   \Gamma |- C : s
----------------------  if x \notin \Gamma
\Gamma, x : C |- x : C
-}

{-
(weak) (s = box)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}

{-
If x == a then the var rule applies and it is used.
If x != a then the var rule does not apply and the weak rule is used instead.
-}

getKind (TypeDeclaration (x, c) : gamma) (TypeVar a) = do
  s <- getBox gamma c
  if s == BoxBox && x `notElem` (getDomain gamma) then
    if x == a then return c else getKind gamma (TypeVar a)
  else Nothing

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getKind (TermDeclaration (x, c) : gamma) (TypeVar a) = do
  s <- getKind gamma c
  if s == KindStar && x `notElem` (getDomain gamma)
  then getKind gamma (TypeVar a)
  else Nothing

getKind [] (TypeVar _) = Nothing


{-
(form) (s = star)
\Gamma |- A : *  \Gamma, x : A |- B : s
---------------------------------------
      \Gamma |- Pi x : A . B : s
-}
getKind gamma (TypePi x a b) = -- a = Type, b = Type
  let gamma' = TermDeclaration (x, a) : gamma in do
    ki_a <- getKind gamma a
    s <- getKind gamma' b
    if ki_a == KindStar && s == KindStar then return s else Nothing

{-
(appl) (type)
\Gamma |- M : Pi x : A . B  \Gamma |- N : A
-------------------------------------------
        \Gamma |- M N : B [x := N]
-}
getKind gamma (TypeApp m n) = do -- m = Type, n = Term
  ki_m <- getKind gamma m
  ty_n <- getType gamma n
  case ki_m of
    KindPi _ a b -> if ty_n == a then return b else Nothing
    _ -> Nothing

{-
(abst) (s = box)
\Gamma, x : A |- M : B  \Gamma |- Pi x : A . B : s
--------------------------------------------------
    \Gamma |- \lambda x : A . M : Pi x : A . B
-}
getKind gamma (TypeAbs x a m) = -- a = Type, m = Type
  let gamma' = TermDeclaration (x, a) : gamma in do
    b <- getKind gamma' m
    s <- getBox gamma (KindPi x a b)
    if s == BoxBox then return (KindPi x a b) else Nothing


-- getType

getType :: Context -> Term -> Maybe Type

{-
(var) (s = star)
   \Gamma |- C : s
----------------------  if x \notin \Gamma
\Gamma, x : C |- x : C
-}

{-
(weak) (s = star)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}

{-
If x == a then the var rule applies and it is used.
If x != a then the var rule does not apply and the weak rule is used instead.
-}

getType (TermDeclaration (x, c) : gamma) (TermVar a) = do
  s <- getKind gamma c
  if s == KindStar && x `notElem` (getDomain gamma) then
    if x == a then return c else getType gamma (TermVar a)
  else Nothing

{-
(weak) (s = box)
\Gamma |- A : B  \Gamma |- C : s
--------------------------------  if x \notin \Gamma
     \Gamma, x : C |- A : B
-}
getType (TypeDeclaration (x, c) : gamma) (TermVar a) = do
  s <- getBox gamma c
  if s == BoxBox && x `notElem` (getDomain gamma)
  then getType gamma (TermVar a)
  else Nothing

getType [] (TermVar _) = Nothing


{-
(appl) (term)
\Gamma |- M : Pi x : A . B  \Gamma |- N : A
-------------------------------------------
        \Gamma |- M N : B [x := N]
-}
getType gamma (TermApp m n) = do -- m = Term, n = Term
  ty_m <- getType gamma m
  ty_n <- getType gamma n
  case ty_m of
    TypePi x a b -> if ty_n == a then return (substituteInType b x n) else Nothing
    _ -> Nothing

{-
(abst) (s = star)
\Gamma, x : A |- M : B  \Gamma |- Pi x : A . B : s
--------------------------------------------------
    \Gamma |- \lambda x : A . M : Pi x : A . B
-}
getType gamma (TermAbs x a m) = -- a = Type, m = Term
  let gamma' = TermDeclaration (x, a) : gamma in do
    b <- getType gamma' m
    s <- getKind gamma (TypePi x a b)
    if s == KindStar then return (TypePi x a b) else Nothing


{-
Examples:

*Main> getType [(TypeDeclaration ("P", (KindPi "x" (TypeVar "A") KindStar))), (TypeDeclaration ("A", KindStar))] (TermAbs "x" (TypeVar "A") (TermAbs "y" (TypeApp (TypeVar "P") (TermVar "x")) (TermVar "y")))
Just (TypePi "x" (TypeVar "A") (TypePi "y" (TypeApp (TypeVar "P") (TermVar "x")) (TypeApp (TypeVar "P") (TermVar "x"))))
-}

[Patrick Thomas]

I have uploaded what I have for the first five chapters of "Type Theory and Formal Proof" to github: https://github.com/pthomas505/ttfp. If anyone has any feedback on things I might have done wrong, or other suggestions, they would be welcome and appreciated. Thank you.