Confusion about coercions

Stream: lean4

[Ioannis Konstantoulas]

In the Functional Programming book, we encounter a coercion from NonEmptyList to List:

instance : Coe (NonEmptyList α) (List α) where
  coe
  | { head := x, tail := xs } => x :: xs

and a claim that 'This allows non-empty lists to be used with the entire List API.' I am not sure what this entails; for instance, I am trying to append two NonEmptyLists and it fails:

def myNeList : NonEmptyList String := ["hello", "my"]
def mySnList : NonEmptyList String := List.append myNeList ["world"]

results in

type mismatch
  List.append ?m.1468 ["world"]
has type
  List String : Type
but is expected to have type
  NonEmptyList String : Type

What am I doing wrong here? Ultimately, I just want to be able to do

def concList : NonEmptyList String := myNeList ++ mySnList

[Ruben Van de Velde]

Well, you're successfully calling List.append and this creates a new List. At this point, lean says "hold on, is that new List really nonempty?" - and this is indeed something you need to prove

[Kyle Miller]

Yeah, it means you can use NonEmptyList wherever a List is expected, but it doesn't mean you can use a List wherever a NonEmptyList is expected.

[Arthur Adjedj]

Coercions allow you to use NonEmptyLists where a List would be expected, but it only goes one way. For example, this definition doesn't give an error:

def myNeList : List String := ({head := "hello", tail := ["my"]} : NonEmptyList String)

If you wanted to do things the other way around, you would need to have a coercion from List to NonEmptyList. This, however, is not possible since you'd also need to coerce empty lists into a nonempty one. If you want to go deeper, there is a way to have some form of such coercion using a dependent coe, called CoeDep:

instance : CoeDep (List α) (x::l) (NonEmptyList α) := ⟨{head := x, tail := l}⟩

Using this, any list that has a term on the head will be able to coerce to a NonEmptyList. This makes your first definition myNeList work. However, it's not so obvious to Lean that your second list mySnList has such a shape, and as such, you'll still get an error on it.

[Kyle Miller]

You could define your own constructor that tries to prove nonemptiness automatically using simp:

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

instance : Coe (NonEmptyList α) (List α) where
  coe
  | { head := x, tail := xs } => x :: xs

def NonEmptyList.ofList (xs : List α) (nonempty : xs ≠ [] := by simp [*]) : NonEmptyList α where
  head := xs.head nonempty
  tail := xs.tail

@[simp]
def NonEmptyList.coe_ofList (xs : List α) (nonempty: xs ≠ []) :
    (NonEmptyList.ofList xs : List α) = xs := by
  cases xs
  · simp at nonempty
  · simp [ofList]

def myNeList : NonEmptyList String := .ofList ["hello", "my"]
def mySnList : NonEmptyList String := .ofList <| List.append myNeList ["world"]
def myNeListOfNeList (neList : NonEmptyList α) : NonEmptyList α := .ofList neList

[Ioannis Konstantoulas]

My problem with all this is that the Functional Programming book is using the above code in the Applicative section:

inductive Validate (ε α : Type) : Type where
  | ok     : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

instance : Coe (NonEmptyList α) (List α) where
  coe
  | { head := x, tail := xs } => x :: xs

instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := { head := x, tail := xs }

instance : Applicative (Validate ε) where
  pure    := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors e =>
      match x () with
      | .ok _ => .errors e
      | .errors e' =>
        .errors (e ++ e') -- NonEmptyList coercion fails to concatenate

This code is directly from that book and it fails. I am not sure what I am missing, since the definitions and instances regarding NonEmptyList are scattered throughout the text.

[Ioannis Konstantoulas]

I wrote an implementation of HAppend for non-empty lists, but the error in the above code persists :(

[Arthur Adjedj]

This works for me:

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

inductive Validate (ε α : Type) : Type where
  | ok     : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

instance : Functor (Validate α):= sorry

instance : Coe (NonEmptyList α) (List α) where
  coe
  | { head := x, tail := xs } => x :: xs

instance : CoeDep (List α) (x :: xs) (NonEmptyList α) where
  coe := { head := x, tail := xs }

instance : Append (NonEmptyList α) where
  append  := λ ⟨x,a⟩ b =>  {head := x, tail := a ++ b}

instance : Applicative (Validate ε) where
  pure    := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors e =>
      match x () with
      | .ok _ => .errors e
      | .errors e' =>
        .errors (e ++ e')

[Arthur Adjedj]

but you're right, it's unfortunate that code coming straigth from the book doesn't work

[Arthur Adjedj]

Looking back at this, I'm having a hard time accepting that this shouldn't work:

structure NonEmptyList (α : Type _) : Type _ where
  head : α
  tail : List α

inductive Validate (ε α : Type _) : Type _ where
  | ok     : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

instance : Functor (Validate α):= sorry

instance : Coe (NonEmptyList α) (List α) where
  coe
  | { head := x, tail := xs } => x :: xs

instance : HAppend (List α) (NonEmptyList α) (NonEmptyList α) where
  hAppend  := λ a b => match a with
    | [] => b
    | x::a =>  {head := x, tail := a ++ b}

instance : Applicative (Validate ε) where
  pure    := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors e =>
      match x () with
      | .ok _ => .errors e
      | .errors e' =>
        .errors ((e : List ε) ++ e')
                                 ^^
/-has type
  List ε : outParam (Type ?u.1962)
but is expected to have type
  NonEmptyList ε : Type ?u.1962-/

Looking into the synthInstances, it looks to me like the outParam of HAppend is decided only upon the first argument (of type List ε), and thus decides this is HAppend (List ε) (List ε) (List ε), before trying to coerce e' into a List. I would naively expect the outParam to take all "non-out" parameters into account before being decided upon. Is this an intended behaviour ? Marking foo as a default_instance doesn't solve the issue either.

[Sebastian Ullrich]

This kind of ambiguous input regarding order of coercions and heterogeneous operations is fundamentally problematic. The heuristic ++ uses to insert coercions fails in this case. https://github.com/leanprover/lean4/blob/a3ebfe29ea516e45dba97dfd303cfc11cc47ff04/src/Lean/Elab/Extra.lean#L91-L96

[Kyle Miller]

I wouldn't suggest to turn off the binop% elaborator here, but in case it's illuminating here's how you do it, and then Lean finds the HAppend instance:

macro_rules | `($x ++ $y) => `(HAppend.hAppend $x $y)

instance : Applicative (Validate ε) where
  pure    := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors e =>
      match x () with
      | .ok _ => .errors e
      | .errors e' =>
        .errors ((e : List ε) ++ e')

[David Thrane Christiansen]

Ioannis Konstantoulas said:

This code is directly from that book and it fails. I am not sure what I am missing, since the definitions and instances regarding NonEmptyList are scattered throughout the text.

This is definitely a drawback of the style!

The code examples that the book's build process draws from are available in its repository. The Append instance is here: https://github.com/leanprover/fp-lean/blob/56422d4a279d6a74dcf6dc1f9eaa84227ea81f0c/examples/Examples/Classes.lean#L1024-L1026

All the book declaration and expect info lines can be ignored - they're part of how the code was extracted.

It would be a nice addition to the book to write a program to extract more readable source to all examples, eliminating the ones with errors.

[Arthur Adjedj]

David Thrane Christiansen said:

Ioannis Konstantoulas said:

This code is directly from that book and it fails. I am not sure what I am missing, since the definitions and instances regarding NonEmptyList are scattered throughout the text.

This is definitely a drawback of the style!

The code examples that the book's build process draws from are available in its repository. The Append instance is here: https://github.com/leanprover/fp-lean/blob/56422d4a279d6a74dcf6dc1f9eaa84227ea81f0c/examples/Examples/Classes.lean#L1024-L1026

All the book declaration and expect info lines can be ignored - they're part of how the code was extracted.

It would be a nice addition to the book to write a program to extract more readable source to all examples, eliminating the ones with errors.

I believe @Ioannis Konstantoulas may have been lead by the exercise given at chapter 4.5 into believing it would make things work, seeing this message:

Ioannis Konstantoulas said:

I wrote an implementation of HAppend for non-empty lists, but the error in the above code persists :(

Perhaps it may help to have one other exercise before the HAppend one to simply prove Append (NonEmptyList α) ? This would be enough to make the code from the book "work"

[David Thrane Christiansen]

Good idea! I'm away from the computer for a bit - would you mind making an issue here? https://github.com/leanprover/fp-lean/issues