Come creare una "classe tipo" in Haskell, o polimorfismo ad hoc a livello di tipo utilizzando famiglie di tipi

Question

Sto studiando le caratteristiche della famiglia di tipi di Haskell e il calcolo del livello di tipo. Sembra che sia abbastanza facile da ottenere il polimorfismo parametrico a livello di tipo utilizzando 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 

posso fare le cose come :kind! Bool == Bool o :kind! Int == Int o :kind! Z == Z e :kind! (I Z (S Z)) == (I (S Z) (S (S Z))).

Tuttavia, desidero rendere il polimero ad-hoc type +. In modo che sia limitato alle istanze che gli ho dato. I 2 esempi qui, sarebbero tipi di tipo NatK e tipi di tipi IntK.

ho provato rendendolo parametricamente polimorfa:

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) 

Questo funziona, come posso fare :kind! (I (S Z) Z) :+ (I (S Z) Z).

Tuttavia, posso anche fare :kind! Bool :+ Bool. E questo non ha alcun senso, ma lo consente come un semplice costruttore di tipi. Voglio creare una famiglia di tipi che non consenta tipi di questo tipo errati.

A questo punto sono perso. Ho provato le classi di tipo con un parametro type. Ma quello non ha funzionato.

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) 

Permette comunque :kind! Add Bool Bool.

Questo ha qualcosa a che fare con l'estensione ConstraintKinds, dove devo limitare lo :+ o Add a qualche "classe gentile"?

Answer 1

La soluzione più semplice è quello di utilizzare le famiglie di tipo aperto per sovraccarico ad hoc e le famiglie di tipo chiuso per l'attuazione:

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 

Se vogliamo più a livello di tipo e durata di livello metodi raggruppate, possiamo scrivere classi tipo utilizzando utilizzando KProxy da Data.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 

Naturalmente, tipi associati sono gli stessi come tipo aperto familie s, così avremmo potuto usare anche famiglie di tipi aperti con una classe separata per i metodi a livello di termine. Ma penso che sia generalmente più pulito avere tutti i nomi sovraccaricati nella stessa classe.

Da GHC 8.0, KProxy diventa inutile in quanto i tipi e tipi saranno trattati esattamente allo stesso modo:

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

(questo dovrebbe essere un commento, ma ho bisogno di più spazio)

ho provato qualcosa di simile

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

ma ho fallito. Non ho idea se ciò che chiedi è realizzabile.

La migliore approssimazione che ho ottenuto è effettuare il controllo di tipo Add Bool Bool, ma generare un vincolo irrisolvibile, in modo che se lo usassimo lo faremo comunque un errore. Forse questo potrebbe essere sufficiente per i tuoi scopi (?).

class Fail a where 

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