1
$\begingroup$

In Lean 4.3.0, I'm solving an exercise from section 4.5 "Standard Classes" of the excellent book "Functional Programming in Lean". Given the structure

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

the exercise is to write an instance of HAppend (List α) (NonEmptyList α) (NonEmptyList α).

Here's a solution that works:

def happ : (List α) → (NonEmptyList α) → (NonEmptyList α)
  | ([] : List α), xs => xs
  | (x :: xs), ys =>
    let ⟨hd, tl⟩ := happ xs ys
    ⟨x, hd :: tl⟩

instance : HAppend (List α) (NonEmptyList α) (NonEmptyList α) where
  hAppend := happ

However, now let's try to implement hAppend directly inside the instance declaration, rather than using a helper function happ. Here's my attempt:

instance : HAppend (List α) (NonEmptyList α) (NonEmptyList α) where
  hAppend : (List α) → (NonEmptyList α) → (NonEmptyList α)
    | ([] : List α), xs => xs
    | (x :: xs), ys =>
      let ⟨hd, tl⟩ := HAppend.hAppend xs ys
      ⟨x, hd :: tl⟩

But this won't pass type checking:

failed to synthesize instance
  HAppend (List α) (NonEmptyList α) ?m.2099

Can anyone explain why?

EDIT:

For comparison, here is the code translated to Haskell, where it type checks with no problem:

-- Haskell code, not Lean

type NonEmptyList a = (a, [a])

class HAppend a b c where
    hAppend :: a -> b -> c

instance HAppend [a] (NonEmptyList a) (NonEmptyList a) where
    hAppend [] xs = xs
    hAppend (x : xs) ys =
        let (hd, tl) = hAppend xs ys
        in (x, hd : tl)
```
$\endgroup$
1
  • $\begingroup$ I think the short answer is that you made up notation which doesn’t work. You want to fill in hAppend with a recursively defined function. If it was a mere case split, I think that that sort of notation would work, but I don’t think Lean support recursive calls inside an instance declaration for only one branch of the declaration. There would be a lot of issues with using HAppend.hAppend as a recursive call in this case. What is your goal here. What do you hope to accomplish? Do you just want to avoid the helper function? $\endgroup$
    – Jason Rute
    Dec 16, 2023 at 14:51

1 Answer 1

1
$\begingroup$

If your goal is to put the helper function happ inside the instance declaration, then I think this is the best approach:

instance : HAppend (List α) (NonEmptyList α) (NonEmptyList α) where
  hAppend := happ
where
  happ : (List α) -> (NonEmptyList α) -> (NonEmptyList α)
  | ([] : List α), xs => xs
  | (x :: xs), ys =>
    let ⟨hd, tl⟩ := happ xs ys
    ⟨x, hd :: tl⟩ 

This isn't specific to instance. You can do this where thing to attach auxiliary definitions to most declarations. See the Binary Search Trees example in the Lean manual.


Another way to inline a recursive definition is with let rec which is like let but allows recursive calls:

instance : HAppend (List α) (NonEmptyList α) (NonEmptyList α) where
  hAppend := 
    let rec happ : (List α) -> (NonEmptyList α) -> (NonEmptyList α)
    | ([] : List α), xs => xs
    | (x :: xs), ys =>
      let ⟨hd, tl⟩ := happ xs ys
      ⟨x, hd :: tl⟩ 
    happ

Note that instances can be recursive but that means something completely different than what you are doing here. Recursive instances work when the types themselves are built from other types. Here List α and NonEmptyList α are built from another type α. We can rely on type class instances for α. This would be a recursive instance:

instance [Add α] : Add (Array α) where
  add x y := Array.zipWith x y (· + ·)

Not only does us let us use + on Array Nat, but on, say, Array (Array (Array (Array Nat))).


The match notation as you wrote does work, but you just cannot use it recursively to fill in a field for an instance. Here is a non-recursive way to define this using that match notation:

instance : HAppend (List α) (NonEmptyList α) (NonEmptyList α) where
  hAppend : (List α) -> (NonEmptyList α) -> (NonEmptyList α)
  | ([] : List α), ys  => ys
  | (x :: xs), ⟨y, ys⟩ => ⟨x, xs ++ [y] ++ ys⟩  -- non-recursive

The only other way I know to inline recursive calls in Lean is to directly call the underlying rec recursor (in this case List.rec), but I would highly discourage doing that.

$\endgroup$
4
  • $\begingroup$ Thanks for the thorough and helpful reply. I agree that 'where' or 'let rec' syntax are nice ways to bring the recursive helper function into the instance declaration. It's also a good point that you don't even need recursion to solve the exercise. Now, it's still a bit surprising to me that an attempt to recursive directly in a function in an instance declaration introduces completely different semantics, i.e. the instance itself becomes recursive as you've pointed out. That would not be the case in Haskell. However, I understand that Lean is not Haskell. :) $\endgroup$ Dec 17, 2023 at 4:53
  • $\begingroup$ By the way I just edited my question above to show a Haskell version of the code. $\endgroup$ Dec 17, 2023 at 4:57
  • $\begingroup$ @AdamDingle I agree it's reasonable for Lean to support notation similar to your Haskell example (and if you think this is important you could make an issue on github). But the notation wouldn't be what you wrote. It would use hAppend instead of HAppend.hAppend. Notice in my where happ example I use happ as the recursive call, not HAppend.happ. Your HAppend.hAppend xs ys is the same as xs ++ ys, so it is closer to the Array example and the non-recursive example where one relies on already having an appropriate instance of HAppend, which in your case hasn't been created yet. $\endgroup$
    – Jason Rute
    Dec 17, 2023 at 14:03
  • $\begingroup$ That's a good point. In fact when I first wrote the code I attempted to recurse using just hAppend xs ys, and only fell back on HAppend.hAppend when that first variant wouldn't type check. I think it would indeed be nice if Lean supported direct recursion in this situation, but don't feel strongly enough about it to make a new issue at this time. :) $\endgroup$ Dec 17, 2023 at 15:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.