type mismatches

Stream: new members

[Joseph O]

I am using lean 4, and I am not sure how to fix this type mismatch:

def nth {α : Type} {αs : List Type} (tup: Tuple (α :: αs)) (n: Nat) :=
  let rec nthAux {α : Type} {αs : List Type} {β : Type} : (tupRest: Tuple (αs)) → (n: Nat) → α
    | (Tuple.cons x xs), 0 => x
    | (Tuple.cons x xs), n+1 => nthAux xs n
  nthAux tup n

Here is the error:

type mismatch
  x
has type
  x✝ : Type
but is expected to have type
  α : Type

Full Source

[Yury G. Kudryashov]

What should be the return type of your definition?

[Joseph O]

Yury G. Kudryashov said:

What should be the return type of your definition?

that is what I can't really figure out

[Yaël Dillies]

WHat are you trying to do, in words?

[Joseph O]

get the nth term of a tuple (a custom datatype i made)

[Adam Topaz]

Please post a #mwe

[Joseph O]

Adam Topaz said:

Please post a #mwe

def foo := ⟪1, "2", 3.0⟫

#eval foo.nth 1 -- "2"

[Adam Topaz]

That's not a #mwe . You can click that link that will take you to a webpage which will explain what is meant by this.

[Joseph O]

import Tuple
open Tuple

def foo := ⟪1, "2", 3.0⟫

#eval foo.nth 1 -- "2"

thats it

[Arthur Paulino]

@Joseph O Adam is asking for a more precise piece of code of yours. You posted a link to your repo, but this link is better: https://github.com/crabbo-rave/lean4-Tuple/blob/master/Tuple.lean

[Joseph O]

Thanks

[Adam Topaz]

def get {αs : List Type} (tup: Tuple αs) (n : Nat) (h : n < αs.length) : αs.get n h :=
match αs, tup, n, h with
| [], Tuple.unit, _, h => absurd h (Nat.not_lt_zero _)
| (a :: as), Tuple.cons x xs, 0, _ => x
| (a :: as), Tuple.cons x xs, (n+1), _ => get xs _ _

def foo : String := (get ⟪2,"foobar",3⟫ 1 sorry)

#eval foo

This is not ideal, because Lean has a hard time figuring out what the type should be (e.g. try #eval (get ⟪2,"foobar",3⟫ 1 sorry)). I don't know off the top of my head how to work around that.

[Adam Topaz]

Note also that your Tuple.length is just the length of the list of types.

[Vincent Beffara]

You can probably emulate std::variant from C++, something like this:

structure variant (ts : tuple_of_types) :=
    (tag : ℕ)
    (val : ts.get tag)

and then discriminate on tag down the line. The std::any version on the other hand,

structure any := (type : Type) (val : type)

is probably useless though si (IIUC) equality between types is something you don't want to do ...

[Vincent Beffara]

And something like the visitor pattern, visitor (ts : tuple_of_types) (out : Type) would be a tuple of the form (ts.get 0 -> out, ts.get 1 -> out, ...),

def visit {ts : tuple_of_types) (f : visitor ts out) (v : variant ts) := (f.get v.tag) v.val

but I'm not sure this typechecks, or is useful if it does

[Vincent Beffara]

Or, maybe something closer to your Tuple implementation like

def value_type : list Type → Type
| [] := unit
| (t :: ts) := t ⊕ value_type ts

[Joseph O]

Would a type class work?