Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Higher-kinded type variables? #446

Open
Zemyla opened this issue Nov 27, 2018 · 6 comments
Open

Higher-kinded type variables? #446

Zemyla opened this issue Nov 27, 2018 · 6 comments

Comments

@Zemyla
Copy link

Zemyla commented Nov 27, 2018

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
Copy link
Member

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
Copy link
Member

edsko commented Nov 28, 2018

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
Copy link
Contributor

facundominguez commented Nov 28, 2018

This was an earlier attempt: haskell-distributed/rank1dynamic#6

Note that this was reverted in 3463a41.

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

@hyperthunk
Copy link
Member

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
Copy link
Member

edsko commented Nov 28, 2018

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

@hyperthunk
Copy link
Member

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.

@LaurentRDC LaurentRDC transferred this issue from haskell-distributed/rank1dynamic Sep 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants