Lean4 blog series

Stream: lean4

[Brandon Brown]

I'm starting a series of blog posts on Lean 4 here: http://outlace.com/Lean_part_1.html
I'm trying to assume the fewest number of prerequisites so it starts very basic.

[Arthur Paulino]

First piece of feedback is that the grey on that light blue hurts my eyes a bit. You might want to increase the contrast between those two colors

[Brandon Brown]

Good point, thank you- I will work on that
Update: fixed

[Henrik Böving]

Also generally style wise we write our types LikeThis, our functions likeThis and our proofs like_this name wise. So your nat should be Nat. Your nat_id natId and so on.

Since that collides with builtins you can just let your blog happen in an example workspace so nothing bad happens.

And UX wise if I open your page on mobile its zoomed in so far per default I can't see ~1/3 of the page.

But both of those are just minor annoyances, the actual content looks good to me!

[Brandon Brown]

Thanks for the feedback! I’ll try to update the code style when I get a chance. I can’t reproduce your mobile issue as it loads and looks fine on my phone even tried different browsers.

[Brandon Brown]

So as I'm writing these posts I'm realizing I'm still confused about some basic things.
Consider the identity function:

def id { α : Type _ } (a : α) := a
#check id -- {α : Type u_1} → α → α

It is polymorphic over the input type α.

If I change it to (not sure why one would want to do this):

def id { α : Prop } (a : α) := a
#check id -- ∀ {α : Prop}, α → α

My understanding is that whenever I see ∀, I'm dealing with a dependent function type. But I thought id here is just polymorphic, not a dependent function type like (x : α) → P x?

[Henrik Böving]

Both denote a dependent function type, it's just that it is convention to use universal quantification once Prop comes into play and the other notation otherwise, the concept of a polymorphic function doesn't really exist separately from a dependent one in Lean. All functions in Lean are created equal.

[Hanting Zhang]

id is dependent in the first argument; id := (α : Prop) → P α where P α := α → α

[Brandon Brown]

Okay, that's what I was thinking, since the output type will depend on the input type. But I then I got confused because in Haskell it's basically the same but Haskell doesn't have dependent types

[Hanting Zhang]

Wait Haskell doesn't have dependent types? What is stuff like head :: forall a. List a -> a then?

[Henrik Böving]

Polymorphic, which is a subset of what is possible in dependent types. THe essential difference is that in dependent type theories your types can refer to values and not just other types

[Hanting Zhang]

Ah I see, thanks

[Brandon Brown]

Posted part 2: http://outlace.com/Lean_part_2.html
Feedback is appreciated! to catch any misstatements or other errors early