Beginner question about lambdas

[chandradeepdey]

I was playing around with the examples in the tutorials and could not make sense of this error.

Why do

let rec append (#a: Type) (l1 l2: list a) : (l: list a {length l = length l1 + length l2}) =
  match l1 with
  | [] -> l2
  | hd :: tl -> hd :: append tl l2

and

let rec append (#a: Type) (l1 l2: list a) : (l: list a {length l = length l1 + length l2}) =
  (fun (l2': list a) ->
      (match l1 with
        | [] -> l2'
        | hd :: tl -> hd :: append tl l2')) l2

work but

let rec append (#a: Type) (l1 l2: list a) : (l: list a {length l = length l1 + length l2}) =
  (fun (l1': list a) ->
      l2': list a
        -> (match l1' with
            | [] -> l2'
            | hd :: tl -> hd :: append tl l2')) l1
    l2

fail with

Expected expression of type "Type"; got expression "l2'" of type "list a" [Ln 5, Col 21]
(See related location: <input>:3:6)

? Why should it be Type?

[TheoWinterhalter]

In your last example you have l2': list a -> ... instead of fun (l2' : list a) -> … so you are indeed writing a function type instead of a function. If you want to write fun only once, then you should write fun (l1' : list a) (l2' : list a) -> ….

[chandradeepdey]

Oh. Thank you so much! This also explains why the formatter kept removing the parentheses around the l2': list a.