Jouer avec des DataKinds - Erreurs de mauvais appariement

Question

J'ai appris à propos de la programmation au niveau du type et je voulais écrire une simple fonction de type addition naturelle. Ma première version qui fonctionne est la suivante:

data Z 
data S n 

type One = S Z 
type Two = S (S Z) 

type family Plus m n :: * 
type instance Plus Z n = n 
type instance Plus (S m) n = S (Plus m n) 

Donc GHCi je peux faire:

ghci> :t undefined :: Plus One Two 
undefined :: Plus One Two :: S * (S * (S * Z)) 

qui fonctionne comme prévu. Je me suis alors décidé d'essayer l'extension DataKinds en modifiant les Z et S types à:

data Nat = Z | S Nat 

Et la famille plus retourne maintenant un Nat genre:

type family Plus m n :: Nat 

Le code modifié compile mais le problème est J'obtiens maintenant une erreur en la testant:

Kind mis-match 
Expected kind `OpenKind', but `Plus One Two' has kind `Nat' 
In an expression type signature: Plus One Two 
In the expression: undefined :: Plus One Two 

J'ai cherché une solution mais Google m'a échoué . Est-ce qu'une solution existe ou ai-je atteint une limite de la langue?

Answer 1

Je pense que la façon dont vous testez n'est pas correcte. undefined peut être de tout type de type * (je me trompe peut-être ici).

Essayez ceci dans ghci

ghci>:t (undefined :: 'Z) 

<interactive>:1:15: 
    Kind mis-match 
    Expected kind `OpenKind', but `Z' has kind `Nat' 
    In an expression type signature: Z 
    In the expression: (undefined :: Z) 

Vous pouvez toujours obtenir le type de Plus One Two en utilisant :kind! dans ghci

ghci>:kind! Plus One Two 
Plus One Two :: Nat 
= S (S (S 'Z))