Pattern matching on Type

Stream: new members

[Sam Cymbaluk]

Hi! I'm trying to create a function that can operate on any kind of type, but mostly returns none. I have this definition:

def F (α : Type) (a : α) : Option Bool := match α with
  | Bool => some (a = true)

but I get the error

type mismatch
  true
has type
  _root_.Bool : Type
but is expected to have type
  α : Type

Is it possible to pattern match on Type? If not, is there some other way to achieve a similar sort of behavior? Thanks!

[Matt Diamond]

Could you explain why you want to write a function that operates on any kind of type?

[Aaron Liu]

I think the closest thing to what you want would be to use a typeclass

[suhr]

Type universes are not inductive types, so you can't match on their elements. But you can define a class.

[Matt Diamond]

A typeclass would work, though I think it would still be good to understand the use case, just to make sure there isn't an #xy problem here

[Sam Cymbaluk]

Thanks for the responses. I'm trying to create a collection of functions with the same type as F that are used for configuring a larger system. The reason for the general type is so that all the functions can be applied the same way, even if some are only concerned with e.g. Bools or Nats. I don't think type classes work because there isn't any shared structure or operation between the elements of Type that I'm interested in. I want access to the type itself so I can use it's particular structure. Something like the Universes of Data from FP in Lean is the closest thing I've found to what I'm trying to do.

[Matt Diamond]

Would this work?

import Mathlib

class CanF (α : Type) where
  F : (a : α) → Option Bool

instance (α : Type) : CanF α where
  F _ := none

instance : CanF Bool where
  F a := some (a = true)

instance : CanF ℕ where
  F n := some (n > 200)

def F {α : Type} [i : CanF α] (a : α) : Option Bool := i.F a

#eval F true
#eval F 123
#eval F "foo"

[Sam Cymbaluk]

Oh, clever! That does work! Out of curiosity, how does Lean know which instance to use? Both CanF α and CanF Bool apply to F true, but the CanF Bool instance is the one "prioritized".

[Matt Diamond]

honestly I'm not sure lol

I suspect there's an answer in this section of the docs: https://lean-lang.org/doc/reference/latest/Type-Classes/Instance-Synthesis/

[Sam Cymbaluk]

From that reference page:

Code that uses instance-implicit parameters should be prepared to consider all instances as equivalent. In other words, it should be robust in the face of differences in synthesized instances.

[Matt Diamond]

Are you quoting that because you're concerned that it means the above code is a bad idea?

[Matt Diamond]

I think this is how it knows which instance is the correct one:

During instance synthesis, if a goal is fully known (that is, contains no metavariables) and search succeeds, no further instances will be attempted for that same goal. In other words, when search succeeds for a goal in a way that can't be refuted by a subsequent increase in information, the goal will not be attempted again, even if there are other instances that could potentially have been used.

The instances for Nat and Bool have no variables... they're maximally specific.

[Matt Diamond]

(I could be misreading that though)

[Sam Cymbaluk]

Mostly sharing that for posterity, but it does seem like it might be a reason to not use the CanF approach. I'm realizing now that the CanF approach doesn't work for me for other reasons. From what I can tell, it limits me to a single function F rather than being able to have a collection of functions from the same family as F. i.e.
a List FConfig

structure FConfig where
  f : (α : Type) → (a : α) → Option Bool

[Mario Carneiro]

I think this is an #xy problem again. Can you give a MWE with the code you want to work?

[Mario Carneiro]

The answer to the earlier question about how to select instances is that you can set priorities, and if the priorities are all default then the last declaration wins. So it's important in Matt Diamond 's example that the none instance comes first. A more idiomatic way to clarify that this is by design is to use instance (priority := low) on that instance.

[Eric Wieser]

Mario Carneiro said:

if the priorities are all default then the last declaration wins.

Is this true? I thought in the face of ties you were at the whim of discrtree key order.

[Robin Arnez]

Yeah it also works like this:

instance : CanF Bool where
  F a := some (a = true)

instance : CanF ℕ where
  F n := some (n > 200)

instance (α : Type) : CanF α where
  F _ := none

Still, discr tree order is deterministic and follows the following (approximate) scheme:

1. Parameters are considered in order of occurrence (earlier ones are considered first)
2. Generalized parameters come before specialized ones
3. For equally specialized variants, the order is exactly insertion order

[Eric Wieser]

I don't understand how to read 2 in the context of your three examples; is the third instance tried before the other two?

[Robin Arnez]

Oh no it's the order in which they are retrieved from the discr tree. Type class search goes through the list in reverse order

[Kenny Lau]

so this is not related to category theory? because that sounds like the mathematically standard way to relate different "types"

[Robin Arnez]

It sounds to me more like this is about polymorphism and not mathematics

[Eric Wieser]

Robin Arnez said:

Type class search goes through the list in reverse order

The "list" being the three instances or the numbered list of three rules?

[Robin Arnez]

List of instances.
Let me make a bigger example:

class CanF (α β : Type) where
  F : α → Option β

instance : CanF Nat β where -- 1
  F _ := none

instance : CanF α Unit where -- 2
  F _ := some ()

instance : CanF α β where -- 3
  F _ := none

instance : CanF Bool Nat where -- 4
  F a := some (if a then 3 else 24)

instance : CanF α α where -- 5
  F x := some x

instance : CanF Bool β where -- 6
  F _ := none

instance : CanF Unit Unit where -- 7
  F a := some a

The order in the discr tree is the following:

1. First all instances with the first parameter generalized (2, 3, 5). 2 has second parameter specialized, so comes after the others: 3, 5, 2
2. Then all instances with first parameter specialized (1, 4, 6, 7). The first one that comes up is Nat: 1
3. The second one that comes up is Bool: first generalized (6), then specialized (4): 6, 4
4. Then Unit: 7

So the discr tree order is: 3, 5, 2, 1, 6, 4, 7. Instance synthesization then takes those of these that match and goes through them in reverse order, so for CanF Bool Nat the order they are tried in is: 4, 6, 5, 3