Différence entre famille de types et newtype partiel? (et des données partielles?)

J'ai dû interfacer deux bibliothèques où les métadonnées sont représentées comme un paramètre de type dans un et comme un champ d'enregistrement dans l'autre. J'ai écrit un adaptateur en utilisant un GADT. Voici une version distillée:Différence entre famille de types et newtype partiel? (et des données partielles?)

{-# LANGUAGE GADTs #-} 

newtype TFId a = MkId a 
data TFDup a = MkDup !a !a 

data GADT tf where 
    ConstructorId :: GADT TFId 
    ConstructorDup :: GADT TFDup 

main = do 
    f ConstructorId 
    f ConstructorDup 

f :: GADT tf -> IO() 
f = _

Cela fonctionne. (Peut ne pas être parfait, les commentaires sont les bienvenus, mais ce n'est pas la question.)

Il m'a fallu du temps pour arriver à cet état de fonctionnement. Mon intuition initiale était d'utiliser une famille de type pour TFId, en supposant: "GADT a genre (* -> *) -> *; dans ConstructorDupTFDup a type * -> *; donc pour ConstructorId je peux utiliser la famille * -> * de type: »

{-# LANGUAGE TypeFamilies #-} 
type family TFId a where TFId a = a

Le constructeur de type a le même genre * -> *, mais GHC apparemment ne l'aura pas au même endroit:

error: …

The type family ‘TFId’ should have 1 argument, but has been given none

In the definition of data constructor ‘ConstructorId’ In the data type declaration for ‘GADT’

Eh bien, si c'est le cas ...

Je ne suis pas sûr de comprendre pourquoi cela ferait une telle différence. Pas d'utilisation de tiges familiales sans les appliquer? Que se passe-t-il? Une autre (meilleure) façon de faire?

Source

2017-09-07 JB.

Oui, les familles de types doivent être utilisées _saturated_ - c'est-à-dire que vous devez appliquer la famille de types à tous ses arguments déclarés. Les familles de types sont développées au moment de la compilation, de sorte que le compilateur doit connaître tous les arguments de la famille de types afin de savoir dans quoi il est censé se développer. La même chose s'applique aux synonymes de type. –

Je serais tenté de faire valoir que les nouveaux types sont développés (bien, réduits) au moment de la compilation, mais avec eux, cela fonctionne. Alors peut-être que le "temps de compilation" est un peu large. Qu'est-ce qui les rend différents?En un mot: pourquoi? –

Bien sûr, j'utilisais le terme "temps de compilation" un peu lâchement. 'newtype's sont effacés lors de la génération de code - la représentation d'un newtype est identique à celle du type wrapped et il est libre de coercer dans les deux sens - mais ils ne sont pas développés lors de la vérification de type comme' type's. 'newtype's sont en dehors de tout autre type; les synonymes de type/familles ne le sont pas. –

Injectivité.

type family F :: * -> * 
type instance F Int = Bool 
type instance F Char = Bool

ici F Int ~ F Char. Cependant,

data G (a :: *) = ...

ne provoquera jamais G Int ~ G Char. Ceux-ci sont garantis être des types distincts.

Dans quantifications universelles comme

foo :: forall f a. f a -> a

f est autorisé à être G (injective), mais ne peuvent pas être F (pas injective).

Ceci sert à faire fonctionner l'inférence. foo (... :: G Int) peut être déduit pour avoir le type Int. foo (... :: F Int) est équivalent à foo (... :: Bool) qui peut avoir le type Int ou le type Char - c'est un type ambigu.

Considérez également foo True. Nous ne pouvons pas nous attendre à ce que GHC choisisse f ~ F, a ~ Int (or Char) pour nous. Cela impliquerait de regarder toutes les familles de types et de voir si Bool peut être produit par n'importe lequel d'entre eux - essentiellement, nous aurions besoin d'inverser toutes les familles de types. Même si cela était faisable, cela générerait énormément de solutions possibles, ce qui serait ambigu.

Source

2017-09-08 08:26:13 chi

Différence entre famille de types et newtype partiel? (et des données partielles?)

Répondre

Questions connexes