Higher-kinded type variables?

Ouverte
  • Quelque chose ne va pas ?
#446 6 commentaires 0 réactions 0 personnes assignées Voir sur GitHub

Personne n'a encore pris cette issue.

Évaluation

Difficulté
5/5
Temps estimé
Plus d'une semaine
Accessibilité débutants
25/100
Type d'issue
Fonctionnalité
Clarté
À clarifier
Activité
À l'abandon
Stack technique
haskell
Domaine
compilers

Piste de recherche

L’issue ne mentionne aucun fichier ni test du dépôt. Commencez par étudier les encodages Any/ANY proposés en Haskell ainsi que le code GHC d’inférence et d’unification auquel elle fait référence. Pour considérer le travail comme terminé, il faudrait une conception et une implémentation concrètes pour les variables Typeable d’ordre supérieur, avec des tests démontrant une inférence et une unification correctes.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Description

enhancement Question rank1dynamic

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.

Langage dominant
Haskell
Étoiles
755
Forks
101
Merge moyen
1 j 3 h
PR mergées (30 j)
4

Préparer son environnement

Par où commencer

  1. Lisez l'issue en entier, puis le guide de contribution du projet.
  2. Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
  3. Forkez le dépôt et travaillez sur une branche.
  4. Ouvrez une pull request qui référence le numéro de l'issue.

Autres issues de haskell-distributed/distributed-process

Toutes les issues de haskell-distributed/distributed-process

Issues similaires

Plus d'issues Haskell

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.