stlc terms

Stream: new members

[Patrick Thomas]

If I understand correctly, in the untyped lambda calculus, we have the inductive definition for terms as something like:

inductive term : Type
| var : var → term
| app : term → term → term
| abs : var → term → term

In this [1] and other formulations of the simply typed lambda calculus I am confused to see this definition unaltered. I had guessed that it would have been amended to incorporate the typing rules somehow. It seems to say that we can have a term of something like app (10) (20)? But then what would its type be? It wouldn't have one by the typing rules right? Doesn't every term have to have a type?
[1] https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html

[Patrick Thomas]

I guess further down in the same document it says that some terms are untypable. I guess programs like Coq and Lean have additional rules to prohibit untypable terms?

[Horatiu Cheval]

Right, in this formulation typing only comes later as some sort of deduction system on these terms, like in the "Typing" section of the book you linked. And then you can start to ask and to prove things like whether a term is well typed, to infer the type of a term (or give an error if it's ill typed), that some operations preserve well typing and so on. And you can indeed have ill typed terms like you point out, but you are generally interested in those well typed

[Horatiu Cheval]

This, if I remember correctly the terminology is sometimes called Curry-style typing.

[Horatiu Cheval]

But you can also implement the types as intrinsic part of the definition of terms, which is Church-style typing

[Patrick Thomas]

Interesting. So Coq and Lean and similar programs use Church style typing?

[Horatiu Cheval]

Where you would have something term : ty -> Type and then app (a b) : term (a --> b) -> term a -> term b so to speak. And this way it will not make sense, by definition to speak of ill typed terms, they don't exist

[Horatiu Cheval]

That I don't know, but I think not, though I'm out of my knowledge zone here

[Patrick Thomas]

Thank you. Is ty a misprint for Type?

[Horatiu Cheval]

No, that would be the simple types of the lambda calculus you are implementing, as opposed to Type, the Lean types, or the types of the system you are implementing it in

[Horatiu Cheval]

So you would have probably an inductive definition of ty saying stuff like "if a and b are types in ty, you can construct a function type in ty"

[Horatiu Cheval]

A function type a --> b I mean, in my notation above, I think I didn't explain that very good

[Patrick Thomas]

I think I see. term is a constructor that takes a ty and returns a Type. And app takes two Types and returns a Type.

[Patrick Thomas]

Is that right?

[Horatiu Cheval]

term would be an inductive type indexed by ty, and ty would be an inductive type.

inductive ty
| some_constant_type : ty
| function_type : ty -> ty -> ty

infixr `==>` : 50 := ty.function_type

inductive term : ty -> Type
| app {a b : ty} : term (a ==> b) -> term a -> term b

[Horatiu Cheval]

Something like this

[Horatiu Cheval]

app takes two terms (of appropriate types, by definition) and returns a term (of appropriate type, by definition)

[Patrick Thomas]

I see. Cool. Thank you!

[Patrick Thomas]

It would be interesting and maybe educational to see what the full formalization of just the simply typed lambda portion of Coq or Lean is, in Coq or Lean. Especially if a user could interact with it in such a way as to manually apply each typing rule, reduction, etc. Basically to see and interact with what is going on behind the scenes. And then see what is changed by adding polymorphism, etc.

[Mario Carneiro]

Patrick Thomas said:

Interesting. So Coq and Lean and similar programs use Church style typing?

Yes. The key difference with church style typing is that a type appears in the term constructor for lambda, \lam x: T, e rather than an unspecified \lam x, e like in your original inductive type

[Patrick Thomas]

How does adding a type in the term constructor for lambda prevent the construction of a term that is not typable, like app (10) (20)?

[Horatiu Cheval]

If I understand Mario correctly I was mistaken in calling my construction there Church typing (or rather, it is Church typing, but you don't need all that for it to count as Church typing), and I should've probably spoken about implicitly vs explicitly typed syntaxes.

[Horatiu Cheval]

So, yes, you can speak of app (10) (20) which is a term even though it is ill-typed

[Patrick Thomas]

I see.

[Patrick Thomas]

Patrick Thomas said:

It would be interesting and maybe educational to see what the full formalization of just the simply typed lambda portion of Coq or Lean is, in Coq or Lean. Especially if a user could interact with it in such a way as to manually apply each typing rule, reduction, etc. Basically to see and interact with what is going on behind the scenes. And then see what is changed by adding polymorphism, etc.

Is this possible, or maybe does it already exist?

[Horatiu Cheval]

Maybe Lean metaprogramming would interest you? I don't know much about it, but if I understand correctly it exposes the Lean implementation of these constructions to you, within Lean, so that you can play around with them and see what happens internally. I don't know about simply typed fragments and so on.

[Horatiu Cheval]

Or do you mean a full formalization in the sense of defining these systems in Lean and proving stuff about them?

[Patrick Thomas]

Yes, a full formalization in Lean or Coq. I'm not as interested in proving stuff about them as in being able to do stuff like see how a term is typed or reduced step by step. Doing something like this more formally:

1. [], [] :: (g : nat -> nat) :: (f : nat -> nat) :: (n : nat) |- g : nat -> nat ; Var
2. [], [] :: (g : nat -> nat) :: (f : nat -> nat) :: (n : nat) |- f : nat -> nat ; Var
3. [], [] :: (g : nat -> nat) :: (f : nat -> nat) :: (n : nat) |- n : nat ; Var
4. [], [] :: (g : nat -> nat) :: (f : nat -> nat) :: (n : nat) |- f n : nat ; App 2 3
5. [], [] :: (g : nat -> nat) :: (f : nat -> nat) :: (n : nat) |- g (f n) : nat ; App 1 4
6. [], [] :: (g : nat -> nat) :: (f : nat -> nat) |- fun n : nat => g (f n) : nat -> nat ; Lam 5
7. [], [] :: (g : nat -> nat) |- fun f : nat -> nat => (fun n : nat => g (f n)) : (nat -> nat) -> (nat -> nat) ; Lam 6
8. [], [] |- fun g : nat -> nat => (fun f : nat -> nat => (fun n : nat => g (f n))) : (nat -> nat) -> ((nat -> nat) -> (nat -> nat)) ; Lam 7

[Johan Commelin]

It sounds like playing around with expr is close to what you want.

[Johan Commelin]

(I.e., the metaprogramming suggestion by Horatiu above.)

[Patrick Thomas]

Hmm. Where could I find more info?

[Johan Commelin]

The tactic writing tutorial, the youtube tutorial on metaprogramming by Rob Lewis, and here on zulip

[Patrick Thomas]

Thank you.

[Johan Commelin]

@Patrick Thomas ooh, you could also work with Lean 4. It's mostly implemented in Lean 4 itself.

[Patrick Thomas]

Nice.

[Patrick Thomas]

I'll take a look.

[Patrick Thomas]

Hmm. It looks like the kernel is in C++.

[Patrick Thomas]

Mario Carneiro said:

Patrick Thomas said:

Interesting. So Coq and Lean and similar programs use Church style typing?

Yes. The key difference with church style typing is that a type appears in the term constructor for lambda, \lam x: T, e rather than an unspecified \lam x, e like in your original inductive type

Do you also mean that Coq and Lean use a formalization like the one given by Horatiu?

inductive ty
| some_constant_type : ty
| function_type : ty -> ty -> ty

infixr `==>` : 50 := ty.function_type

inductive term : ty -> Type
| app {a b : ty} : term (a ==> b) -> term a -> term b

[Mario Carneiro]

No, application does not have type arguments. See expr.app. But lambda does.

[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) =
  case (getType gamma tm1, getType gamma tm2) of
    (Just (Arrow ty11 ty12), Just ty2) ->
      if ty11 == ty2 then Just ty12 else Nothing
    _ -> Nothing
getType gamma (Abs v ty1 tm1) =
  let gamma' = Data.Map.insert v ty1 gamma in
  case getType gamma' tm1 of
    Just ty2 -> Just (Arrow ty1 ty2)
    _ -> Nothing


{-
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

[Notification Bot]

This topic was moved by Mario Carneiro to #Type theory > stlc terms

[Patrick Thomas]

I'm not sure what happened. If I click on the topic in Type theory there is no history.

[Patrick Thomas]

and getType _ trivial = Just True?

[Mario Carneiro]

you sure about that?

[Mario Carneiro]

I see the history, try reloading

[Patrick Thomas]

Ok. Yes, needed to reload.