No support for polymorphism over record fields

[duvenaud]

My simplex demo needs an Eq instance for a particular record type. I managed to make one by hand, but is it possible in the current codebase to make a generic constructor of Eq or other typeclasses for records?

For example, here's the instance for Eq for pairs:

@instance
def pairEq (eqA: Eq a)?=> (eqB: Eq b)?=> : Eq (a & b) = MkEq $
  \(x1,x2) (y1,y2). x1 == y1 && x2 == y2

I started trying to write an analogous one for records, but because I can't refer to the names of the fields explicitly (or somehow quantify over them), I think it's impossible.

[apaszke]

Yeah I thought about it some time ago, and concluded that I don't see an easy fix right now, so I moved on. cc @danieldjohnson

[danieldjohnson]

Yeah, this seems hard to do right now. I think that doing this properly would require something like type families / associated types / typeclass functional dependencies, so that you could unpack a record in a generic way without knowing its fields in advance.

[apaszke]

FWIW type families already work, because types are values just like any other and you can store them in typeclasses:

data To64Bit a:Type =
  MkTo64Bit Type

@instance upcastInt32 : To64Bit Int32 = MkTo64Bit Int64
@instance upcastInt64 : To64Bit Int64 = MkTo64Bit Int64

def getUpcast (a : Type) -> (d : To64Bit a) ?=> : Type = case d of MkTo64Bit t -> t

getUpcast Int32

[danieldjohnson]

Well, they sort of work, in that you can write them down. But type inference can't reduce through them so you can't actually do anything interesting with them:

data To64Bit a:Type = MkTo64Bit t:Type (a->t)

@instance upcastInt32 : To64Bit Int32 = MkTo64Bit Int64 IToI64
@instance upcastInt64 : To64Bit Int64 = MkTo64Bit Int64 id

def GetUpcast (a : Type) -> (d : To64Bit a) ?=> : Type = case d of MkTo64Bit t _ -> t

:p GetUpcast Int32
> Int64

def upcast (a : Type)?-> (d : To64Bit a) ?=> (v : a) : (GetUpcast a) =
  (MkTo64Bit _ fn) = d
  fn v
> Type error:Can't reduce type expression: (GetUpcast a)
>
> def upcast (a : Type)?-> (d : To64Bit a) ?=> (v : a) : (GetUpcast a) =
>                                                   ^

[apaszke]

Fair enough, but I don't think that this is a fundamental difficulty. We should just make the reduction more powerful.

[danieldjohnson]

I think it's a bit more fundamental than that, since this also violates a bunch of our internal assumptions:

• the core IR requires that all types are Atoms, but GetUpcast a isn't one
• we assume that the type of anything can be computed without emitting any decls (i.e. using getType) but getting the type of upcast {a} {d} v requires actually running GetUpcast, which does an unpack (and in general could do more complicated things too)
• we do dictionary synthesis as a separate pass after type inference, but for anyone who uses upcast, the result of type inference depends on the results of dictionary synthesis
• our core unification algorithm doesn't have any support for non-injective Type -> Type functions

I think each of these could be solved or worked around but the solution doesn't seem straightforward to me. (But I agree that this is something we should support!)

[duvenaud]

I too like the idea of making type inference more powerful, but would that allow a solution to the record instances problem? I don't see how the necessary type families could be written without being able to refer to the names of fields.

[danieldjohnson]

Not on its own, but the solution I imagined to the record problem involves type families. I was thinking something like Haskell's Generic typeclass, e.g.

interface Generic a where
  rep : Type  -- note: this isn't actually in scope in lower decls but I'm writing it this way anyway
  toGeneric : a -> rep
  fromGeneric : rep -> a

and then the compiler would automatically solve something like Generic {a:A & b:B & c:C} with rep = GenericRecord A {b:B & c:C}. Then you could write typeclass instances for records in terms of this:

instance _ : Generic {&...r} ?=> Eq (rep {&...r}) ?=> Eq {&...r} where ...

instance _ : Eq a ?=> Eq b ?=> Eq (GenericRecord a b) where ...

I suppose that this isn't strictly necessary to write typeclasses for records either, we could have the generic thing happen in the compiler itself whenever it tries to solve for an instance of a record, or something. (edit: although I'm not sure that actually works, because then the compiler has to figure out how to transform an instance for GenericRecord into one for the actual record, which might not always be obvious)

[danieldjohnson]

Hm. But if we need to have the compiler write stuff for us anyway, maybe there's a way to do it without the type families if we design the transformation in the right way... I'll think on it some more and see if I come up with something.

I was wondering if we could get away with something like

data KnownRecord a = EmptyRecord (Iso a {}) | HasSomeField f:Type rest:Fields (Iso a (f & {...rest}))

and having the compiler solve KnownRecord specially (so that you could use it with ?=>), then use that to implement other typeclasses. But this doesn't work, because the type f is inside the value, so there's no way to write a constraint like

instance _ : (d:KnownRecord a) ?=> Eq (?????) ?=> Eq a where
   eq = case d of ...

because we don't know what equality constraints we need to solve (Eq (?????)) until we can unpack the KnownRecord.

[apaszke]

@danieldjohnson Wouldn't your last proposal work if you parametrized KnownRecord by f and rest as well? After all you want to constrain those types to have an Eq instance.

[apaszke]

About your earlier arguments about GetUpcast: I do agree that there is some difficulty in that we might not be able to normalize the type ahead of time, because dictionary synthesis will be unable to provide us with a concrete instance in a polymorphic function. So we would have to start allowing Exprs as types, but it might be an extension we should go for at some point anyway.

[danieldjohnson]

I don't think that quite works, because the "caller" is supposed to bind all of the arguments to the typeclass ADT. If we had something like

instance _ : f:Type ?-> rest:Fields ?-> KnownRecord f rest full
                    ?=> Eq f ?=> Eq {&...rest} ?=> Eq {&...full}
    where ....

then in order to solve Eq {&...full} we would first need to solve KnownRecord f rest full, but f and rest are universally quantified in this definition so there's no way to solve it for only a single specific f and rest. (This is where something like functional dependencies could come in as an alternative solution, by letting us say that f and rest depend on full instead of being universally quantified. But I'm not sure functional dependencies make sense as a more general dependently-typed abstraction.)

Regarding Exprs as types, I had hoped that #179 would help with that. Hopefully we can figure out a way to do it that doesn't break too much.