Zulip Chat Archive

Stream: general

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


Kaushik Chakraborty (Jul 30 2021 at 15:33):

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 (Jul 30 2021 at 15:36):

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 (Jul 30 2021 at 15:40):

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 (Jul 30 2021 at 17:18):

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 (Jul 30 2021 at 17:38):

yeah, because in dependent type theory, types are terms

Mac (Jul 30 2021 at 17:54):

@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 (Jul 30 2021 at 17:56):

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 (Jul 30 2021 at 17:58):

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

Mac (Jul 30 2021 at 17:58):

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

Mario Carneiro (Jul 30 2021 at 17:59):

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 (Jul 30 2021 at 17:59):

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 (Jul 30 2021 at 18:00):

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 (Jul 30 2021 at 18:01):

yes it's open. Why does that matter?

Mario Carneiro (Jul 30 2021 at 18:02):

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

Mario Carneiro (Jul 30 2021 at 18:03):

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

Mac (Jul 30 2021 at 18:03):

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 (Jul 30 2021 at 18:04):

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

Mac (Jul 30 2021 at 18:04):

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 (Jul 30 2021 at 18:06):

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 (Jul 30 2021 at 18:07):

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

Mario Carneiro (Jul 30 2021 at 18:15):

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 (Jul 30 2021 at 18:21):

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 (Jul 30 2021 at 18:22):

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 (Jul 30 2021 at 18:40):

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 (Jul 30 2021 at 20:17):

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 (Jul 30 2021 at 20:30):

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 (Jul 30 2021 at 20:30):

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

Kyle Miller (Jul 30 2021 at 23:21):

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 (Jul 30 2021 at 23:32):

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 (Jul 30 2021 at 23:41):

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 (Jul 31 2021 at 16:49):

@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 (Jul 31 2021 at 17:00):

@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 (Jul 31 2021 at 17:03):

@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 (Jul 31 2021 at 17:06):

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

Mac (Jul 31 2021 at 18:19):

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 (Jul 31 2021 at 18:22):

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 (Jul 31 2021 at 18:41):

@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 (Jul 31 2021 at 18:44):

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 (Jul 31 2021 at 22:15):

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 (Jul 31 2021 at 22:17):

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 (Aug 01 2021 at 18:26):

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 (Aug 01 2021 at 18:30):

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 (Aug 01 2021 at 18:33):

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 (Aug 01 2021 at 18:34):

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 (Aug 01 2021 at 21:39):

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 (Aug 01 2021 at 21:54):

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 (Aug 01 2021 at 22:25):

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 (Aug 03 2021 at 05:49):

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 (Aug 03 2021 at 05:54):

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 (Aug 03 2021 at 06:08):

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 (Aug 03 2021 at 16:40):

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)


Last updated: Dec 20 2023 at 11:08 UTC