recursing over nd homogenous array

Stream: general

[Frederick Pu]

Hi, I'm trying to make a helper function for converting an nd homogenous list to a string, but get the following error, does anyone have any tips on how to fix this?

-- n nested homogenous Array
inductive NArray (α : Type u) : Nat → Type u where
| nil (n : Nat) : NArray α n
| cons₁ (a : α) (l : NArray α 1) : NArray α 1
| cons₂ {n : Nat} (a : NArray α n) (l : NArray α (n+1)) : NArray α (n + 1)

def aux {α : Type} [ToString α] {n : Nat} : NArray α n → String
| NArray.nil n  => ""
| NArray.cons₁ a (NArray.nil 1) => toString a
| NArray.cons₁ a l => toString a ++ ", " ++ aux l
| NArray.cons₂ a (NArray.nil (n + 1))=> "[" ++ aux a ++ "]"
| NArray.cons₂ a l => "[" ++ aux a  ++ "]" ++ ", " ++ aux l
/-
application type mismatch
  a.cons₂ (NArray.nil (n + 1))
argument
  NArray.nil (n + 1)
has type
  NArray ?m.1350 (n + 1) : Type ?u.1349
but is expected to have type
  NArray α (?m.1348 + 1) : Type
-/

[Miyahara Kō]

Short answer: Try this

def aux {α : Type} [ToString α] {n : Nat} : NArray α n → String
| NArray.nil n  => ""
| NArray.cons₁ a (NArray.nil 1) => toString a
| NArray.cons₁ a l => toString a ++ ", " ++ aux l
| NArray.cons₂ (n := n) a (NArray.nil .(n + 1))=> "[" ++ aux a ++ "]"
| NArray.cons₂ a l => "[" ++ aux a  ++ "]" ++ ", " ++ aux l

[Frederick Pu]

what is the (n := n) notation ?

[Kevin Buzzard]

https://lean-lang.org/lean4/doc/lean3changes.html#function-applications

[Miyahara Kō]

Long answer:
This is because Lean can't infer n as an argument of NArray.cons₂, which is implicit argument.
So, we should tell Lean that n is an implicit argument of NArray.cons₂, writing (n := n).
(continue)

[Frederick Pu]

ohhh
so this also works then:

def aux {α : Type} [ToString α] {n : Nat} : NArray α n → String
| NArray.nil n  => ""
| NArray.cons₁ a (NArray.nil 1) => toString a
| NArray.cons₁ a l => toString a ++ ", " ++ aux l
| NArray.cons₂ a (NArray.nil (_ + 1))=> "[" ++ aux a ++ "]"
| NArray.cons₂ a l => "[" ++ aux a  ++ "]" ++ ", " ++ aux l

[Frederick Pu]

or this:

def aux {α : Type} [ToString α] {n : Nat} : NArray α n → String
| NArray.nil n  => ""
| NArray.cons₁ a (NArray.nil 1) => toString a
| NArray.cons₁ a l => toString a ++ ", " ++ aux l
| NArray.cons₂ a (NArray.nil _)=> "[" ++ aux a ++ "]"
| NArray.cons₂ a l => "[" ++ aux a  ++ "]" ++ ", " ++ aux l

[Miyahara Kō]

(continued from my last post)
However, Lean gives an error that the same argument can't be used twice now.
So, we mark n + 1 by .(n + 1), which tells Lean that no new arguments are here.

[Frederick Pu]

im still kinda confused by what that means tho

[Miyahara Kō]

I was also confused at first, but after writing complex pattern matching, I naturally understood it, so it is no problem even if I don't understand it very well now:+1:

[Frederick Pu]

im sure ill deal with similar stuff in the future lol

[Miyahara Kō]

Let's look at a more obvious example.
Let's define an empty list of natural number.
List.nil is often used in the form of [].

def myList := List.nil

This causes error because Lean can't infer whose type is this list, in other word, Lean doesn't know what is α:

inductive List (α : Type u) where
  | nil : List α
  | cons (head : α) (tail : List α) : List α

So we tell Lean that α is Nat, writing (α := Nat).

def myList := List.nil (α := Nat)

[Frederick Pu]

so the := allows you to specify a specific implicit parameter without having to specify all of them?

[Ruben Van de Velde]

yes

[Frederick Pu]

so in this case : | NArray.cons₂ (n := n) a (NArray.nil .(n + 1)), the first n := n specifies the implicit parameter for the cons_2 and the .(n + 1) makes it so that implicit parameter is also used for the Narray.nil?

[Frederick Pu]

ig my other question would be where the n on the right hand side of n := n comes from, is that the one from the top of function declaration {n : Nat}?