A few basic types are:
- Bool
- Nat
- Float
You define constants with the following syntax:
def j : Nat = 3
def k : Bool = falseThere's some auxiliary commands such as:
#check: which type checks an expression#eval: which evaluates an expression
These are ways of interacting with the system.
The Bool type seems to have two values: true and false. That makes sense.
However when playing with #check I accidentally typed True instead of
true and noticed that it's not invalid, and True is in fact of type Prop.
That's fascinating and makes quite a lot of sense. It's an atomic proposition
which always takes the value true, and of course, False exists too. Fun!
I have not yet tried using Lean with neovim, but from the browser version
(which uses monaco and bundles Lean's extension, I suppose), typing symbols
like ∧ seems to work in a way similar to LaTeX, you type \and (notice: it's not
\land but \and, for some reason. I mean, it makes sense: you don't have other
and symbols, but it kills muscle memory.). Further note: you can also use &&
(and is so far preferred by the book)
Let a and b be types. A function from a to b (i.e. a function that
takes an input of type a and returns one of type b), is typed a → b.
def a := Nat
def b := Nat
#check a -> b -- a → b : Type(1: the : Type part seems to be the...type of the type? or well, the type of the
return value of #check maybe, but I might be wrong)
(2: YES! types are first class citizens, seemingly. so, you can make constants which are types. FUN!!!)
Need more inputs? Cartesian product. Observe:
a × b -> cThe above is the type of a function that takes two inputs, one of type
The strikethrough above is actually what you may perceive it as, but it's not
accurate:a and one of type
b, and returns an output of type c.
The above is the type of a function which takes a single input and returns a
single output. The input's type is a ordered pair, where the first element is
of type a and the second is of type b. The output is of type c.
def a := Nat
def b := Nat
def c := (a × b) -> Type
#check c -- Type 1ooh. Yeah, I don't know what that means, but it's not erroring... so..... yes?...
Don't wanna write a × b? You can just.......... use an .... sigh infix
operator called Prod. Observe:
#check a × b -- a × b : Type
#check Prod a b -- a × b : TypeFun question to ask: is this an operator or a function? (or both? although that's more of a philosophical question)
Funner quesetion to ask: how could we craft a proposition that determines
whether two objects -- in our case, types -- are equal? This would simplify the
above text into one line which would output true or false, showing whether
the two syntaxes are equivalent.
I had forgotten that this is not just types... you can have values, and you can have values that are pairs. Silly me. Here's a pair:
#check (1, 3.5) -- Nat × FloatI'm sure this makes loads of sense but I can't quite wrap my head aroudn this right now:
#check (3, (3, (3, (3, (3, (3)))))) -- (3, 3, 3, 3, 3, 3) : Nat × Nat × Nat × Nat × Nat × Nat#eval (5, 9).1 -- 5There's also .fst and .snd
#check Nat.succWhat type do you think this returns? Nat -> Nat? Yeah, that's what I'd think.
Hell, just to be nice I'd say Nat -> Nat : Type.
But noooooooo, it's (n : Nat) : Nat.
My understanding is that for some stupid reason n here is the name of the
input, which is useless on the type level. Nat (the first one) is the type
of the input, that makes sense. And Nat (the alst one) is the return type?
BUT WHAT HAPPENED TO ->?!?!?!
The good thing is that if you let Lean interpret this, it will say
Expected type: ⊢ Nat → Nat
Which is good, but leaves questions about what #check really does.
Hey, okay, here it is:
#check Nat.succ 4 -- Nat.succ 4 : NatYeah, makes sense, I suppose, but wait a minute hold on. Why is Nat.succ 4
there? uhhhhhhhhhhhhhhhh. Wait, how does this link back to my previous rant?
Could it, perhaps, be there for the same reason (n: Nat) was there? ohhhh,
right. For whatever reason n is named (perhaps I can do that with Nat.succ 4 here as welll) and it's just... telling me the type, but in a weird way. I
truly don't now what it gives me still though.
#check Nat → Nat → Nat -- Nat → Nat → Nat : TypeThis is slang for, a function that takes a Nat and returns a funciton that
takes a Nat and returns a Nat. Even though I knew of the concept of
currying and expected it to be here I had trouble with this, but it makes sense
now.
The reason I had trouble is because, why the hell do we have two mechanisms of providing more than one input to a function? we have ordered pairs, and now we have currying. They achieve the same thing, but in different ways, right? and well, currying has a lot more applications and general advantages, too.
Behold, Nat.Add.
#check Nat.add -- Nat.add : Nat → Nat → Nat
#check Nat.add 3 1 -- Nat.add 3 1 : Nat
#check Nat.add 3 -- Nat.add 3 : Nat → NatI love currying, actually. So, when you provide one argument, it removes one level of the function chain, sorta.
That's a word I came up with, don't quote me.
Some expanding on the type system and how types are first class citizens:
#check Bool -- Bool : TypeNotice how Bool, a type, is of type... Type!
And of course,
#check Type -- Type : Type 1What happens when you
#eval Bool
```?
I like the error message, it reads:cannot evaluate, types are not computationally relevant
Oh yeah, remember `Prod` from earlier? you're not gonna believe this, but it's
a ~~function~~, and operates on types. HELL YES!
#check Prod -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
NOTE: I have read further and at this point... I don't know if it's a
function... (maybe a parametrized type of sorts?)
Okay that's big to unpack, I'll check on it later and see if I get it then.
Basically my point is that the type is actually `Type -> Type -> Type`.
You can check this by creating a constant of which you explicitly define the
type rather than letting Lean infer it, and setting its value to `Prod`! If it
errors, you're wrong. If it doesn't, ding ding ding!
```lean
def P : Type -> Type -> Type := Prod -- No errors!
List is a type which from what I understand takes a type parameter of sorts.
That, or it's a function that returns a type. That's the approach Zig takes
from what I gather, and I think it's quite clean! Not sure which one it is though.
Anyway.
def NatList := List Nat
#check NatList -- NatList : TypeGosh that's a beautiful concept.
Earlier I stumbled upon the fact that Type is of type Type 1.
Turns out that Type 1 is of type Type 2, which is of type Type 3, and so
on, until... not sure, but it's infinite.
Type 0 is a universe of, from what I gather, simple types.
Type 1 is larger, and contains Type 0 as an element!
Naturally, Type 2 is even larger and contains Type 1 as an element.
Type is an abbreviation of Type 0
So, every Type n is of type Type n+1.