Comment créer une "classe kind" dans Haskell, ou un polymorphisme ad-hoc au niveau type en utilisant des familles de types

Question

J'étudie les caractéristiques de famille de types de Haskell, et le calcul de niveau type. Il semble qu'il est assez facile d'obtenir polymorphisme paramétrique au niveau de type en utilisant PolyKinds:

{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators, UndecidableInstances, PolyKinds, MultiParamTypeClasses, FlexibleInstances #-} 

data NatK = Z | S NatK 
data IntK = I NatK NatK 

infix 6 + 
type family (x :: NatK) + (y :: NatK) :: NatK where 
    Z  + y = y 
    (S x) + y = S (x + y) 

-- here's a parametrically polymorphic (==) at the type-level 
-- it also deals specifically with the I type of kind IntK 
infix 4 == 
type family (a :: k) == (b :: k) :: Bool where 
    (I a1 a2) == (I b1 b2) = (a1 + b2) == (a2 + b1) 
    a == a = True 
    a == b = False 

Je peux faire des choses comme :kind! Bool == Bool ou :kind! Int == Int ou :kind! Z == Z et :kind! (I Z (S Z)) == (I (S Z) (S (S Z))).

Cependant, je veux faire type + polymorphe ad-hoc. Alors que c'est contraint aux instances que je lui donne. Les 2 instances ici, seraient les types de type NatK et les types de type IntK.

J'ai d'abord essayé de faire ce paramétriquement polymorphes:

infix 6 :+ 
type family (x :: k) :+ (y :: k) :: k where 
    Z   :+ y = y 
    (S x)  :+ y = S (x :+ y) 
    (I x1 x2) :+ (I y1 y2) = I (x1 :+ y1) (x2 :+ y2) 

Cela fonctionne, comme je peux le faire :kind! (I (S Z) Z) :+ (I (S Z) Z). Mais je peux aussi faire :kind! Bool :+ Bool. Et cela n'a aucun sens, mais il le permet comme constructeur de type simple. Je veux créer une famille de types qui n'autorise pas de tels types errants.

À ce stade, je suis perdu. J'ai essayé des classes de type avec un paramètre type. Mais cela n'a pas fonctionné.

class NumK (a :: k) (b :: k) where 
    type Add a b :: k 

instance NumK (Z :: NatK) (b :: NatK) where 
    type Add Z b = b 

instance NumK (S a :: NatK) (b :: NatK) where 
    type Add (S a) b = S (Add a b) 

instance NumK (I a1 a2 :: IntK) (I b1 b2 :: IntK) where 
    type Add (I a1 a2) (I b1 b2) = I (Add a1 b1) (Add a2 b2) 

Il permet toujours :kind! Add Bool Bool.

Est-ce que cela a quelque chose à voir avec l'extension ConstraintKinds, où je dois contraindre le :+ ou Add à une certaine "classe aimable"?

Answer 1

La solution la plus simple est d'utiliser des familles de type ouvert pour la surcharge ad hoc et les familles de type fermé pour la mise en œuvre:

data NatK = Z | S NatK 
data IntK = I NatK NatK 

type family Add (x :: k) (y :: k) :: k 

type family AddNatK (a :: NatK) (b :: NatK) where 
    AddNatK Z b = b 
    AddNatK (S a) b = S (AddNatK a b) 

type family AddIntK (a :: IntK) (b :: IntK) where 
    AddIntK (I a b) (I a' b') = I (AddNatK a a') (AddNatK b b') 

type instance Add (a :: NatK) (b :: NatK) = AddNatK a b 
type instance Add (a :: IntK) (b :: IntK) = AddIntK a b 

Si nous voulons à plusieurs niveaux de type et des méthodes de niveau terme regroupés, nous pouvons écrire des classes nature à l'aide à l'aide de KProxyData.Proxy:

class NumKind (kproxy :: KProxy k) where 
    type Add (a :: k) (b :: k) :: k 
    -- possibly other methods on type or term level 

instance NumKind ('KProxy :: KProxy NatK) where 
    type Add a b = AddNatK a b 

instance NumKind ('KProxy :: KProxy IntK) where 
    type Add a b = AddIntK a b 

Bien sûr, les types associés sont les mêmes que type ouvert familie s, donc nous aurions pu aussi utiliser des familles de type ouvert avec une classe séparée pour les méthodes au niveau terme. Mais je pense qu'il est généralement plus propre d'avoir tous les noms surchargés dans la même classe.

De GHC 8.0, KProxy devient inutile puisque les types et les types seront traités de la même manière exacte:

{-# LANGUAGE TypeInType #-} 

import Data.Kind (Type) 

class NumKind (k :: Type) where 
    type Add (a :: k) (b :: k) :: k 

instance NumKind NatK where 
    type Add a b = AddNatK a b 

instance NumKind IntK where 
    type Add a b = AddIntK a b 

Answer 2

(Cela devrait être un commentaire mais j'ai besoin de plus d'espace)

J'ai essayé quelque chose comme

class GoodK (Proxy k) => NumK (a :: k) (b :: k) where ... 

mais j'échoué. Je n'ai aucune idée si ce que vous demandez est réalisable.

La meilleure approximation que j'ai obtenue est de faire Add Bool Bool, mais générer une contrainte insoluble, de sorte que si nous l'utilisons, nous aurons une erreur de toute façon. Peut-être que cela pourrait être suffisant pour vos besoins (?).

class Fail a where 

instance Fail a => NumK (a :: *) (b :: *) where 
    type Add a b =()