{-# LANGUAGE DataKinds, ExistentialQuantification, KindSignatures #-}
import Data.Proxy
data Type t= forall (a :: t). Type (Proxy a)
donne l'erreurPourquoi la quantification existentielle et les datakinds ne fonctionnent-ils pas ensemble?
Type variable ‘t’ used in a kind
In the kind ‘t’
In the definition of data constructor ‘Type’
In the data declaration for ‘Type’
Mais t est une variable genre, pas une variable de type. Que se passe-t-il?
Les arguments des constructeurs de type sont des types et non des types. Donc data Type t = ... signifie t est une variable de type. Dans GHC 8.0, l'extension TypeInType supprime la distinction entre les types et les types, permettant à votre programme d'être accepté si vous l'activez (et GHC proposera d'activer l'extension si ce n'est pas le cas).
Avant le GHC 8, aucune liaison de type n'est autorisée, où que ce soit. Ici, nous devons utiliser des proxies aimables. Dans ce cas, nous pouvons faire:
import Data.Proxy
data Type (kp :: KProxy k) = forall (a :: k). Type (Proxy a)
Avec GHC 8, vous pouvez en effet écrire votre version originale:
{-# language TypeInType #-}
data Type t = forall (a :: t). Type (Proxy a)
Je ne suis pas sûr que cette définition exacte fonctionne dans GHC 8, puisque Type est intégré – bennofs
Je viens juste de l'essayer et ça marche dans ghci Nous obtenons seulement 'Type' si nous importons' Data.Kind'. –
Vous ne pouvez pas mélanger encore les types et les types dans la syntaxe concrète. Le mieux que vous pouvez faire est 'Type de données (tp :: KProxy t) = forall (a :: t). Tapez (Proxy a) '(bien que je ne vois pas à quel point ce type de données serait utile, mais c'est un problème tout à fait différent.) – user2407038