Haskell's closed type families as Lean's inductive family

Stream: general

[Kaushik Chakraborty]

I am trying to encode this closed type family encoded in Haskell in Lean 4. I think it can be done via Inductive Type families but since I am absolutely novice in these advanced type system encodings, not able to figure out. Any help would be appreciated. Thanks

type family ElementOf a where
  ElementOf [[a]] = ElementOf [a]
  ElementOf [a]   = a

[Mario Carneiro]

Type families like this cannot directly be represented in lean, because type constructors are not necessarily injective. But you can do something similar with typeclasses

[Mario Carneiro]

class ElementOf (α : Type u) where
  El : Type u

instance : ElementOf (List α) := ⟨α⟩
instance [ElementOf (List α)] : ElementOf (List (List α)) :=
  ⟨ElementOf.El (List α)⟩

example : ElementOf.El (List α) = α := rfl
example : ElementOf.El (List (List α)) = α := rfl
example : ElementOf.El (List (List (List α))) = α := rfl

[Kaushik Chakraborty]

thanks. so when in Haskell it is said that type family is kind of a function from types to types and type classes are function from types to terms, in Lean type classes can do both right.

[Mario Carneiro]

yeah, because in dependent type theory, types are terms

[Mac]

@Mario Carneiro One limitation though is that you can't pattern match on types in Lean, though, right? Whereas that is what closed type families essentially do in Haskell.

That is, the closest approximation in Lean of a closed type family would be something like:

def ElementOf!.{u} : Type u → Type u
| List (List α) => ElementOf! (List α)
| List α => α
| _ => panic! "invalid type"

But this doesn't work because you can't pattern match on types in Lean.

[Mario Carneiro]

What does that pattern match look like in haskell? This is a bit semantically weird so I don't know exactly how it's handled

[Mario Carneiro]

If you want to define a function out of a type family, you can add it as a field in the typeclass above

[Mac]

The difference is that a type class is open whereas a closed type family is, well, closed.

[Mario Carneiro]

It is possible to define an inductive type family that only holds at certain types, but it's not actually as useful as you would think

[Mac]

Mario Carneiro said:

What does that pattern match look like in haskell?

That pattern match is what the closed type family example @Kaushik Chakraborty gave does.

[Mario Carneiro]

okay but I already gave an approximate equivalent for that code snippet. I'm hoping for something that shows what aspect of the haskell version is missing from the lean version

[Mario Carneiro]

yes it's open. Why does that matter?

[Mario Carneiro]

that panic! in your version also looks bad. Is that what the haskell version does too?

[Mario Carneiro]

I don't think it makes sense for the haskell code to have a panic! in a type

[Mac]

Mario Carneiro said:

that panic! in your version also looks bad. Is that what the haskell version does too?

I added the panic! match since the original example is missing a catch-all alternative )which iirc would be required in Haskell).

[Mario Carneiro]

Are you sure? I think it is just a partial function, like a typeclass

[Mac]

Mario Carneiro said:

I don't think it makes sense for the haskell code to have a panic! in a type

No, actually, Haskell does support panicing in types. It is called a TypeError.

[Mac]

Mario Carneiro said:

Are you sure? I think it is just a partial function, like a typeclass

No it is not. Closed type families are complete. That is the entire point of them in Haskell. :P
However, You can cheat this with the TypeError I just mention much like in Lean you could with panic!.

[Mac]

Also, for reference, here is the GHC User Guide section on closed type families.

[Mario Carneiro]

unfortunately that section doesn't say anything about what you can do with closed type families, it just describes the declaration, which seems pretty well handled by those instances in the lean version

[Mac]

My argument was not that the Lean analogue of closed type families would be necessary useful, just simply that a type class with instances is not it. :rolling_on_the_floor_laughing: Also, your example could be translate d back into Haskell using associated (open) type families (which attach a type to a type class just like you did).

[Mac]

Such an example would look something like this in Haskell:

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}

class ElementOf a where
  type El a

instance {-# OVERLAPPABLE #-} ElementOf [a] where
  type El [a] = a

instance {-# OVERLAPPING #-} ElementOf [[a]] where
  type El [[a]] = El [a]

[Mac]

Having now tested my example on GHC 8.6, it doesn't compile because Haskell doesn't support overlapping open type family alternatives. This made me remember that one of the key uses of closed type families in Haskell is to deal with such cases. As Lean is much more okay with overlap, at least that concern does not exist.

[Anatole Dedecker]

Mario Carneiro said:

class ElementOf (α : Type u) where
  El : Type u

instance : ElementOf (List α) := ⟨α⟩
instance [ElementOf (List α)] : ElementOf (List (List α)) :=
  ⟨ElementOf.El (List α)⟩

example : ElementOf.El (List α) = α := rfl
example : ElementOf.El (List (List α)) = α := rfl
example : ElementOf.El (List (List (List α))) = α := rfl

In this exemple, there would be two diferent instances of ElementOf (list (list nat)), right ? One with nat and one with list nat ?

[Mario Carneiro]

Yes. The order of the two instances is significant; you can also get the same effect by marking the first instance as (priority := low)

[Mario Carneiro]

That is, we are relying on typeclass inference to always apply the second instance when possible

[Kyle Miller]

Here's an attempt at something like a closed type family (in Lean 3), using has_coe_to_sort as a small convenience. It requires that you say how a type is constructed, in the form of a term of ElementOf.dom. I implemented a generic flatten with it as a small test.

inductive ElementOf.dom
| incl (α : Type*) : ElementOf.dom
| list (f : ElementOf.dom) : ElementOf.dom

namespace ElementOf

def dom.to_sort : dom → Type*
| (dom.incl α) := α
| (dom.list f) := list (dom.to_sort f)

instance : has_coe_to_sort ElementOf.dom := ⟨_, ElementOf.dom.to_sort⟩

def dom.apply : dom → dom
| (dom.incl α) := dom.incl α
| (dom.list f) := dom.apply f

end ElementOf

def flatten : Π {α : ElementOf.dom} (x : α), list α.apply
| (ElementOf.dom.incl α) x := [x]
| (ElementOf.dom.list f) x := list.bind x flatten

[Kyle Miller]

I don't have much experience with them, but maybe this is a place where unification hints can be used to automatically generate the ElementOf.dom term.

[Eric Wieser]

My memory was that unification hints were entirely broken in lean3 for anything using universe variables, and only really worked for Type not Type*

[Mac]

@Kyle Miller's example inspired me and led me to this implementation (in Lean 4):

class inductive Elem.{u} : (α : Type u) → (β : outParam $ Type u) → Type (u+1)
| flat (h : α = β) : Elem α β
| list (γ : Type u) (h : α = List γ) (tail : Elem γ β) : Elem α β

instance : Elem α α := Elem.flat rfl
instance [e : Elem α β] : Elem (List α) β := Elem.list α rfl e

abbrev ElemOf.{u} (α : Type u) [Elem α β] :=
  β

#reduce ElemOf (List (List Nat)) -- Nat

def flattenAux (a : α) : Elem α β → List β
| Elem.flat h => [cast h a]
| Elem.list γ h e => List.bind (cast h a) fun x => flattenAux x e

def flatten (a : α) [e : Elem α β] : List β :=
  flattenAux a e

#reduce flatten [[0], [1]] -- [0, 1]

[Kyle Miller]

@Mac Nice idea with the class inductive. You can get rid of the type equalities:

class inductive Elem : (α : Type u) → (β : outParam $ Type u) → Type (u+1)
| incl : Elem α α
| list (tail : Elem α β) : Elem (List α) β

instance : Elem α α := Elem.incl
instance [e : Elem α β] : Elem (List α) β := Elem.list e

abbrev ElemOf (α : Type u) [Elem α β] := β

#reduce ElemOf (List (List Nat)) -- Nat

def flattenAux : Elem α β → (a : α) → List β
| Elem.incl, a => [a]
| Elem.list tail, a => List.bind a fun x => flattenAux tail x

def flatten (a : α) [e : Elem α β] : List β :=
  flattenAux e a

#reduce flatten [[0]] -- [0]
#reduce flatten [[[1,2]]] -- [1, 2]

[Mac]

@Kyle Miller I personally like including the type equalities because it makes it so you don't have to rely on the sometimes finicky nature of match generalizing

[Kyle Miller]

I'd rather make sure match generalizes properly than to deal with cast, but I suppose it's a matter of taste.

[Mac]

I guess as a person who does a decent amount of systems programming, casting between types is a very natural operation for me. In fact, implicit casts kind of bothers me.

[Mac]

That is, I would intuitively expect the a in the match to have the same type as the a outside it. The generalizing nature of match is often very counter-intuitive for me.

[Kyle Miller]

@Mac The cast function tends to be annoying to deal with when you have to prove anything about your definitions, since you've put yourself on the road toward heterogeneous equalities, or worse, trying to prove that two types are not equal (which is impossible most of the time).

If it makes you feel any better, in this case the match "reveals" what α actually was (and the a : α in the type signature was unnecessary -- I removed it). It's letting you deconstruct α and then, for example with Elem.list, reinterpret a as having type List α', since that's the type it actually had.

[Kyle Miller]

It can be made more explicit:

def flattenAux : Elem α β → α → List β
| Elem.incl (α := α), (a : α) => [a]
| Elem.list (α := α') tail, (a : List α') => List.bind a fun x => flattenAux tail x

[Mac]

Kyle Miller said:

It's letting you deconstruct α and then, for example with Elem.list, reinterpret a as having type List α'

The 'reintepret' is what I have a problem with. For me, that should always require an explicit cast (it even somewhat annoys me that Lean does this automatically with things like defs). However, I do realize that it is often a necessary part of the Lean.

Kyle Miller said:

Mac The cast function tends to be annoying to deal with when you have to prove anything about your definitions, since you've put yourself on the road toward heterogeneous equalities, or worse, trying to prove that two types are not equal (which is impossible most of the time).

My proofing experience has mostly been with logical systems of my own design so I sadly don't have much experience with proving things about practical functions like these. However, I am curious as to what is the problem with heterogenous equalities? Also, are there significant problems with augment inter- or intra- type equalities with additional axioms (i.e. ones that state terms from two distinct types are equal or that state that two types are not equal)?

[Mac]

I know that additional axioms in a mathematical may often be an anathema. But in program verification contexts, I don't imagine it is as much of one.

[Mario Carneiro]

ones that state terms from two distinct types are equal

It's not possible to say this in lean in any nontrivial way. Heterogeneous equality HEq a b (or a == b in lean 3) asserts that a and b have the same type and when you cast along that type equality the elements are equal. So terms of distinct types are never HEq.

[Mario Carneiro]

Mac said:

Kyle Miller said:

It's letting you deconstruct α and then, for example with Elem.list, reinterpret a as having type List α'

The 'reintepret' is what I have a problem with. For me, that should always require an explicit cast (it even somewhat annoys me that Lean does this automatically with things like defs). However, I do realize that it is often a necessary part of the Lean.

There is no cast because we aren't actually talking about a single variable a; in each case there is a different variable with a different type, and the fact they are both called a is only due to our naming sense. This is shadowing at best, there is no actual relation between the a variables inside and outside the match

[Mario Carneiro]

However, I am curious as to what is the problem with heterogenous equalities?

The main problem with heterogeneous equalities is that they don't accomplish as much as you would expect of equality in an extensional type theory; in particular you can rarely rewrite with them, and it's incredibly difficult to use them at all without carefully chosen motives in the recursor

[Mario Carneiro]

The main reason for this is that the lemma f == g -> x == y -> f x == g y does not hold in lean (it's independent)

[Kyle Miller]

Mac said:

The 'reintepret' is what I have a problem with. For me, that should always require an explicit cast

You can think of a match expression as a way to do an explicit cast, in the sense of a C# is type pattern (for example, if (a is string s) { ... do something with s ... }). The analogy is somewhat clearer if you write the match explicitly:

def flattenAux (t : Elem α β) (a : α) : List β :=
match t, a with
| Elem.incl, a' => [a']
| Elem.list (α := α') t', (a' : List α') => List.bind a' fun x => flattenAux t' x

The second case is something like a made-up if (a is list<α'> a') { ... do something with a' ... }. (Though Lean needs the t to drive this -- I wasn't sure of a good way to render the dependent types in C#!)

[Kyle Miller]

Mario Carneiro said:

in an extensional type theory

In proof assistants with an extensional type theory, in practice how do you change the type of a term to something equal? A while back I tried reading some of the NuPRL documentation, since ncatlab says it's extensional, but I couldn't find anything about that.

(An idle curiosity: are there proof assistants that let you dynamically add reduction rules given proofs of equalities? This would be one way to make equal things defeq.)

[Mario Carneiro]

Like I mentioned to Steven in the other thread, in Mizar (which uses set theory as the foundation but has a soft type system), there a command to say reconsider x as B [by ...]; which amounts to the proof rule |- x : A, |- A <= B => |- x : B, where the by is a proof that A is a subset of B, where A is the "current" type of x as determined by the typechecker. I believe you can also give the newly type ascribed x a different name so that you can use x at either the old or new type.

[Mac]

Mario Carneiro said:

The main reason for this is that the lemma f == g -> x == y -> f x == g y does not hold in lean (it's independent)

If its independent, should you be able to safely do axiom heq_trans : f == g -> x == y -> f x == g y if needed?

[Mac]

Mario Carneiro said:

ones that state terms from two distinct types are equal

It's not possible to say this in lean in any nontrivial way. Heterogeneous equality HEq a b (or a == b in lean 3) asserts that a and b have the same type and when you cast along that type equality the elements are equal. So terms of distinct types are never HEq.

Is there anything preventing one from defining a new proper truly type heterogenous equality that does have the desired properties (either constructively or with axions)?

[Mac]

Kyle Miller said:

Mac said:

The 'reintepret' is what I have a problem with. For me, that should always require an explicit cast

You can think of a match expression as a way to do an explicit cast, in the sense of a C# is type pattern (for example, if (a is string s) { ... do something with s ... }). The analogy is somewhat clearer if you write the match explicitly:

def flattenAux (t : Elem α β) (a : α) : List β :=
match t, a with
| Elem.incl, a' => [a']
| Elem.list (α := α') t', (a' : List α') => List.bind a' fun x => flattenAux t' x

!)

I get what it is doing, I just don't like it. In my view, match's only effect should be pattern matching -- not type juggling. Thus a and a' should have the same type unless otherwise (explicitly) specified. However, your example does have an explicit cast in the form of the type ascription, so I am much more okay with it than I am with the implicit magic of a normal match.

[Mario Carneiro]

Mac said:

Mario Carneiro said:

The main reason for this is that the lemma f == g -> x == y -> f x == g y does not hold in lean (it's independent)

If its independent, should you be able to safely do axiom heq_trans : f == g -> x == y -> f x == g y if needed?

Well, it is closely related to injectivity of pi (if you only consider the types of the variables in the heqs) which is false in general because of Prop (\forall x: Nat, true is equal to \forall x: Unit, true by propositional extensionality)