Type Classes vs Dependent functions

Stream: new members

[Juan Pablo Romero]

I'm trying to understand better the kind of things one can do with type classes vs dependent functions. For example, consider this definition of tuples:

inductive Tuple : List Type -> Type 1
  | tnil : Tuple []
  | tcons (h: H) (t: Tuple T) : Tuple (H :: T)

infixr:67 " *: " => Tuple.tcons
notation "[" "]" => Tuple.tnil

Now I want to write a function to get a value given the type. This is straightforward with type classes:

class Getter (ts: List Type) (A) where
  apply: Tuple ts -> A

def get (t: Tuple ts) A [g: Getter ts A]: A :=
  g.apply t

instance: Getter (A :: T) A where
  apply := fun | h *: _ => h

instance [g: Getter T A]: Getter (B :: T) A where
  apply := fun | _ *: t => g.apply t

def t1: Tuple [Char, String, Int] :=
  'c' *: "a" *: 1 *: []

example: get t1 String = "a" := rfl

At some point one needs to check if the head's type is the same as the user provided type A.

Is that even possible using plain (or dependent) functions?

[Jason Rute]

Juan Pablo Romero said:

Is that even possible using plain (or dependent) functions?

Dependent functions need to be polymorphic. So you can't define a polymorphic function of signature

def get (t: Tuple ts) A: A

since that would be inconsistent (if say A wasn't in ts and A was empty). I do however believe you could define a function of the form

def get A (t: Tuple (ts0 ++ [A] ++ ts)) : A

but I don't think that would be as useful to you.

[Juan Pablo Romero]

Interesting ... so for this to work the list of types would have to be constructed in a very particular way (in some kind of tree: left [A] right)

[Jason Rute]

(Parenthetical:) Note that your type-class driven get function would return different results based on the presentation of the type list ts.

def t2: Tuple [Char, String, String] :=
  'c' *: "a" *: "b" *: []

def t3: Tuple [Char, String, id String] :=
  'c' *: "a" *: "b" *: []

example: t2 = t3 := rfl.              -- t2 and t3 are equal tuples using different presentations of their types
example: get t2 String = "b" := rfl
example: get t3 String = "a" := rfl

[Jason Rute]

Juan Pablo Romero said:

Interesting ... so for this to work the list of types would have to be constructed in a very particular way (in some kind of tree: left [A] right)

I don't think so. I'm just too lazy to fill in the function but my second get should work as written. It will return the nth element of the tuple, where n = ts0.length + 1.

[Juan Pablo Romero]

A few questions: why do you need to insert id in t3?

[Jason Rute]

By replacing String with id String, I'm changing how the type class system sees the type of the third element of t3. Your type class instance doesn't cover this case, so it skips id String and goes to String in the second element of the tuple.

[Jason Rute]

To be clear, id is just the identity function that does nothing but return the inner value.

[Juan Pablo Romero]

Now I'm a bit confused: I was convinced that matching the list of types happened from left-to-right, but it seems that's not the case :thinking:

[Jason Rute]

I think in the [Char, String, String] case both your first and second instances apply, so it is just whichever one that Lean happens to pick first. In other words, the behavior might be deterministic, but I'm not sure it is predictable. It probably isn't "safe" to use a Tuple with a repeated type with this type class.

[Juan Pablo Romero]

true... I was assuming that the more similar pattern would match first (as it happens in Scala), but that might not be the case.
Thanks for the insights!

[Jason Rute]

I've seen people use HLists in Scala to good effect, and I think this could be very useful for programming as long as one avoids some of the rough edges (like multiple repeated types or using type aliases), but when I've seen people use HLists, they always use unique custom types and don't repeat types (at least if they are using Types to organize and refer to the elements of the HList). Then this would work great.

[Jason Rute]

Also, I'm not an expert on the ordering of type class resolution in Lean 4 and how consistent it is. Here is the paper, https://arxiv.org/abs/2001.04301 on how it works, but I don't know if it addresses such minutia. For questions about the order of resolution, it might be good to ask in the #lean4 stream.

[Juan Pablo Romero]

Found the answer to resolution order in the docs:
"... Instances which are declared last are tried first ..."
Mystery solved.

[Damiano Testa]

I'm not sure if this heuristic applies in your specific case, but it is common for stuff in Lean to be resolved/inferred/parsed right-to-left (or last-to-first), rather than left-to-right (or first-to-last).

I suspect that the underlying reason is that with dependent types, the later a term appears, the more information its type is likely to contain, since, to even write it down, you may need everything that came earlier.

[Mario Carneiro]

I think it has more to do with the fact that the local part of the environment is stored as a List (because we want to be able to persist earlier versions of the environment for interactivity reasons), and so the last things added are the most easily accessible

[Jason Rute]

I think it is also important to take newer or more local type class instances into account first. This lets one explicitly override a type class instance in a special circumstance for the duration of some local scope. In Scala 2, this is appomplished for implicit resolution (Scala’s version of type class resolution) through some complicated precedence ordering:

1. First look in current scope

   • Implicits defined in current scope
   • Explicit imports
   • wildcard imports

2. Now look at associated types in

   • Companion objects of a type
   • Implicit scope of an argument's type (2.9.1)
   • Implicit scope of type arguments (2.8.0)
   • Outer objects for nested types
   • Other dimensions

Lean seems to just follow the simpler approach of looking backward in declaration order which probably gives much of the same behavior.

[Jason Rute]

Wait, I didn't think this through. Unlike Scala, I don't think there is a way to "locally scope" a type class instance, so one probably doesn't want to override type class instances like one can do in Scala.

#eval @default Nat _ -- 0
section foo
instance nat_has_inhabited2 : Inhabited Nat := ⟨ 42 ⟩   -- change default value
#eval @default Nat _ -- 42
end foo
#eval @default Nat _ -- 42 (still 42 outside the scope of this section, and for every file which imports this one?)

[Yaël Dillies]

What about local instance?

[Juan Pablo Romero]

yeah doing

local instance nat_has_inhabited2 : Inhabited Nat := ⟨ 42 ⟩

will restore the original value (0) when the scope ends.

[Junyan Xu]

Lean seems to just follow the simpler approach of looking backward in declaration order which probably gives much of the same behavior.

So should we order imported files from the most elementary to the most advanced? I think currently we usually order them alphabetically.