Higher-kinded type variables?

[Zemyla]

I find myself wanting to be able to Typeable quantify over higher-kinded variables, like * -> * or Constraint. This problem comes in two parts: one of them I've thought a lot about and I'm pretty sure I've cracked, and one of them I haven't been able to swing at successfully.

{-# LANGUAGE PolyKinds, DataKinds, EmptyDataDecls, MultiParamTypeClasses, UndecidableInstances, UndecidableSuperclasses #-}
import GHC.TypeLits (Nat)
import qualified GHC.Exts as E (Any)

There's two different approaches, which depend on what version of GHC you have. The first is the simpler, if you have a newer version.

data family Any :: Nat -> k -- Not exported
type family ANY :: Nat -> k where -- Exported
  ANY = Any

Unlike the type family Any from GHC.Exts, the data family here is Typeable.

The other works if you have an older version which can't declare data families ending in anything other than *.

data AnyT0 (n :: Nat) -- None of these datatypes are exported.
data AnyT1 (n :: Nat) (a :: k)
data AnyT2 (n :: Nat) (a :: ka) (b :: kb)
-- And so on.
class E.Any => AnyC0 (n :: Nat) -- And neither are these.
class E.Any => AnyC1 (n :: Nat) (a :: k)
class E.Any => AnyC2 (n :: Nat) (a :: ka) (b :: kb)
type family ANY :: Nat -> k where -- This is, though.
  ANY = AnyT0
  ANY = AnyT1
  ANY = AnyT2
  ANY = AnyC0
  ANY = AnyC1
  ANY = AnyC2
  -- And so on.

This is also more convenient because you use GHC-provided Nats rather than bespoke Peano nats.

The problem I'm having, and the reason this is an issue rather than a pull request, is I don't know how to do inference and unification on these types. I suspect you'd need something similar to GHC's code for it.

[hyperthunk]

The problem I'm having, and the reason this is an issue rather than a pull request, is I don't know how to do inference and unification on these types. I suspect you'd need something similar to GHC's code for it.

Neither do I, unfortunately. Another considering is how many older GHC releases we want to support. For distributed-process, which is the primary consumer of rank1dynamic in Cloud Haskell, the oldest GHC version we're going to be supporting is GHC-7.10.3. Not sure if that impacts you here on not...

As for how to unify on these types, @facundominguez / @edsko - can either of you shed any light on this?

[edsko]

I think higher kinds should be relatively easy to add, if I am not mistaken. Higher rank types is a significantly more difficult challenge. But I think for extending it to type variables of kinds other than * -> * should be fairly straightforward. But it's possible that I'm overlooking something here :)

[facundominguez]

This was an earlier attempt: #6

Note that this was reverted in 3463a41.

Haven't checked how compatible the implementation there is with the approaches discussed here.

[hyperthunk]

Going forwards, I'm not sure if we should be standardising on static pointers (since we no longer support GHC < 7.10 in distributed-process, would that makes this problem go away?), or merging the static-closure and distributed-static libraries to support both static pointers and the current manually constructed remote tables...?

[edsko]

I think requiring support for static pointers and dropping the RemoteTables is perfectly reasonable and would make the situation for CH much cleaner.

[hyperthunk]

I think requiring support for static pointers and dropping the RemoteTables is perfectly reasonable and would make the situation for CH much cleaner.

Thanks for the feedback, @edsko - I think the same thing. I also want to look at whether we should split up the representations of data passed between programs, and static pointers + closures.

If I'm simply passing data types back and forth, it would be nice if I didn't have to have all the nodes running the same executable. I'm wondering whether switching to serialise and sharing the same library code would be a reasonable approach to doing that? Ideally we'd like GHC to provide some support for being able to determine that a remote source of serialised values is compatible with our code.

Using static pointers is obviously far more restrictive, and I think two nodes which are passing closures in this way to one another should refuse to attempt to decode values unless they're from a node which is verifiably running the same program. Again, I think we need GHC to help with this.