A few basic types are:
- Bool
- Nat
- Float
You define constants with the following syntax:
def j : Nat = 3
def k : Bool = false
There'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 -> c
The 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 1
ooh. 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 : Type
Fun 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 × Float
I'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 -- 5
There's also .fst
and .snd
#check Nat.succ
What 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 : Nat
Yeah, 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 : Type
This 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 → Nat
I 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 : Type
Notice how Bool
, a type, is of type... Type
!
And of course,
#check Type -- Type : Type 1
What 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 : Type
Gosh 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
.