So erstellen Sie eine "Art-Klasse" in Haskell oder Ad-hoc-Polymorphismus auf der Ebene der Typ-Typen

Question

Ich untersuche die Typ-Familie Features von Haskell, und geben Sie Level-Berechnung. Es scheint, es ist ganz einfach, parametrischen Polymorphismus bei dem Art-Level zu erreichen mit 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 

ich Dinge wie :kind! Bool == Bool oder :kind! Int == Int oder :kind! Z == Z und :kind! (I Z (S Z)) == (I (S Z) (S (S Z))) tun können.

Allerdings möchte ich type + ad-hoc polymorph machen. Damit ist es auf die Instanzen beschränkt, die ich ihm gebe. Die 2 Instanzen hier wären Typen der Art NatK und Typen der Art IntK.

Ich versuchte zunächst, es parametrisch polymorphen machen:

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) 

Dies funktioniert, wie ich :kind! (I (S Z) Z) :+ (I (S Z) Z) tun können.

Allerdings kann ich auch :kind! Bool :+ Bool tun. Und das macht keinen Sinn, aber es erlaubt es als einfacher Typ Konstruktor. Ich möchte eine Typfamilie erstellen, die solche fehlerhaften Typen nicht zulässt.

An diesem Punkt bin ich verloren. Ich habe Klassen mit einem type Parameter versucht. Aber das hat nicht funktioniert.

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) 

Es erlaubt immer noch :kind! Add Bool Bool.

Hat dies etwas mit der ConstraintKinds Erweiterung zu tun, wo ich die :+ oder Add auf einige "Art-Klasse" beschränken müssen?

Answer 1

Die einfachste Lösung offener Typ Familien für Ad-hoc-Überlastung und geschlossene Familien für die Umsetzung zu verwenden ist:

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 

Wenn wir gruppiert mehrere Typ-Ebene und Begriff Ebene Methoden wollen zusammen, wir können solche Klassen schreiben KProxy von Data.Proxy mit Verwendung:

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 

natürlich assoziierten Arten die gleichen wie offene Art sind familie s, also hätten wir auch offene Typfamilien mit einer separaten Klasse für Methoden auf Termebene verwenden können. Aber ich denke, es ist im Allgemeinen sauberer, alle überladenen Namen in derselben Klasse zu haben.

Von GHC 8.0 wird KProxy unnötig, da Arten und Typen, die genau die gleiche Art und Weise behandelt werden:

{-# 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

(Dies sollte ein Kommentar sein, aber ich mehr Platz benötigen)

Ich habe versucht, so etwas wie

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

aber ich gescheitert. Ich habe keine Ahnung, ob das, was du verlangst, erreichbar ist.

Die beste Approximation, die ich bekommen habe ist Add Bool Bool Art-Check, aber erzeugen eine unlösbare Einschränkung, so dass, wenn wir es jemals verwenden werden wir einen Fehler trotzdem bekommen. Vielleicht könnte dies für Ihre Zwecke (?) Ausreichen.

class Fail a where 

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