fp-lean
fp-lean copied to clipboard
leanprover
Polymorphism typos and minor nits
occaisionally => occasionally
head! is used with no earlier explanation of what the ! means. I think it would be helpful to add a reminder after this paragraph that in Lean "?", "!" are not special operators, they are simply part of the name of a method, leans allows these special characters to be used as part of an identifier. Therefore it is really only a "naming convention" that ? means Optional and "!" means "undo the optional part if you can". I found this very confusing coming from C# where "?" is an actual operator meaning the type to the left is now nullable, until Leo explained it to me.
Prod could mention C# Tuple<T,Q,...>
Sum could mention C "unions"
Sum inl - Leo told me it means "insert left" and "insert right", but I might have misheard...
Sum section doesn't show how to make a Sum value and should add there is no syntactic sugar for making such values.
Unit ==> For instance, a List Unit does not contain anything interesting, but it can express how many entries are expected, and they can be inserted later.
Can you say more about this? I don't get it...
==> Additionally, a function that takes Unit as an argument is a way to express a block of code that can be executed on-demand.
Can you say more about this? I don't get this either?
Empty ==> with a value at type Empty. => You've used this "at type" language a couple times, I keep wanting to read it "of type...". What does "at type" mean?
Naming: Sums, Products, and Units ==> very helpful, thanks!
Messages you may meet ==> "For now, try making the type an argument to the inductive type as a whole, rather than to the constructor."
I tried it:
inductive MyType (α : Type) : Type where
| ctor : α → MyType
but it also produces an error:
type expected
failed to synthesize instance
CoeSort (Type → Type) ?m.99
Message you may meet ==> "For technical reasons, allowing these datatypes could make it possible to undermine Lean's use as a logic."
What does "use as a logic" mean? How about saying "Lean currently does not allow this for technical reasons."
Exercise on zip, I made the jump in pattern matching that it can handle multiple arguments to figure this out, but probably because I've read lots of Lean code by now. Now sure real noobs will figure that out, this is covered in the next section under Pattern-Matching Definitions, so perhaps this exercise should be moved to 1.7?
match xs, ys with
| [], b => []
| b, [] => []
| a :: t, b :: u => (a, b) :: zip t u
and if we mention pattern matching is order sensitive then one can write the more compact version Lean has:
def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
match xs, ys with
| a :: t, b :: u => (a, b) :: zip t u
| _, _ => []
I needed some help with this one:
- Write a function that shows how 2 × x = x + x. It should have type Bool × α → α ⊕ α.
What is the Bool here? You have not yet discussed how a proof is really just a special kind of def that operates on propositions, but I assume that's not what you are asking here, even though the language leads me down that path...?
Sum could mention C "unions"
I don't want to do this, because Sum is a single generic way of writing down tagged unions in general, while the C unions that I've seen are typically encodings of particular tagged unions.
The error that you got from MyType was due to a missing type argument alpha in the constructor. I've added that error message to the section :-)
For zip, I was expecting a solution like this:
def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
match xs with
| [] => []
| x :: xs' =>
match ys with
| [] => []
| y :: ys' => (x, y) :: zip xs' ys'
I think that this uses no features not yet introduced.
I rewrote the instructions on the 2 * x = x + x bit. Is it clearer now?
Can you say more about this? I don't get it...
The example wasn't great, so I replaced it with something more realistic.
For
zip, I was expecting a solution like this
Hello @david-christiansen , for what it's worth, I wrote:
def zip {α β : Type} (xs : List α) (ys : List β) : List (α × β) :=
match (xs, ys) with
| (x :: xrest, y :: yrest) => {fst := x, snd := y} : (zip xrest yrest)
| _ => []
… which failed with a termination error. It seems like this can be solved using Simultaneous Matching according to https://proofassistants.stackexchange.com/questions/2407/proof-of-termination-for-zip-in-lean, but that's introduced in the next chapter. Perhaps it would be better to mention this in chapter 1.5 instead?
Thanks!
Sorry for the slow turnaround, but the imminent release fixes this issue. Thank you!