GADT: Y at-il une raison pour laquelle le type le plus faible ou le plus fort n'est pas choisi

Question

Je lis Fun With Phantom Types. Le premier exercice demande pourquoi il est nécessaire de fournir une signature aux fonctions opérant sur les types fantômes. Bien que je ne peux pas trouver une raison générale, je ne vois un problème dans l'exemple suivant:

data Expr a where 
    I :: Int -> Expr Int 
    B :: Bool -> Expr Bool 
    Add :: Expr Int -> Expr Int -> Expr Int 
    Eq :: (Eq a) => Expr a -> Expr a -> Expr Bool 


whatIs (I _) = "an integer expression" 
whatIs (Add _ _) = "an adition operation" 

Maintenant, je comprends qu'il ya deux types possibles pour whatIs ci-dessus, à savoir:

Expr a -> String 

et

Expr Int -> String 

cependant, le compilateur donne lieu une erreur:

• Couldn't match expected type ‘t’ with actual type ‘[Char]’ 
    ‘t’ is untouchable 
     inside the constraints: t1 ~ Int 
     bound by a pattern with constructor: I :: Int -> Expr Int, 
       in an equation for ‘whatIs’ 
     at ti.hs:9:9-11 
    ‘t’ is a rigid type variable bound by 
    the inferred type of whatIs :: Expr t1 -> t at ti.hs:9:1 
    Possible fix: add a type signature for ‘whatIs’ 
• In the expression: "someString" 
    In an equation for ‘whatIs’: whatIs (I _) = "someString" 
• Relevant bindings include 
    whatIs :: Expr t1 -> t (bound at ti.hs:9:1) 

Je me demande pourquoi le compilateur ne choisit aucun des deux.

Answer 1

Pour votre exemple, Expr a -> String est un type strictement mieux que Expr Int -> String: partout où un Expr Int -> String pourrait être utilisé, un Expr a -> String fera certainement. Mais parfois n'est pas un type "le plus faible" ou "le plus fort".

simplifions votre exemple encore plus loin:

data SoSimple a where 
    SoSimple :: SoSimple Int 

eval SoSimple = 3 :: Int 

Maintenant, voici deux bons types parfaitement pour donner eval:

eval :: SoSimple a -> a 
eval :: SoSimple a -> Int 

Ces types ne sont pas interchangeables! Chacun est utile dans différentes situations. Comparez:

{-# LANGUAGE EmptyCase #-} 
{-# LANGUAGE GADTs #-} 
import Data.Void 

data SomeSimple where 
    SomeSimple :: SoSimple a -> SomeSimple 

-- typechecks if eval :: SoSimple a -> Int, 
-- but not if eval :: SoSimple a -> a 
evalSome :: SomeSimple -> Int 
evalSome (SomeSimple x) = eval x 

-- typechecks if eval :: SoSimple a -> a, 
-- but not if eval :: SoSimple a -> Int 
evalNone :: SoSimple Void -> Void 
evalNone = eval 

Ainsi, ni d'entre eux est plus général que l'autre (et il se trouve que aucun type est plus général que les deux tout en laissant se eval typecheck). Comme il n'y a pas de type le plus général pour eval, il est logique de refuser de choisir un type et de forcer l'utilisateur à décider lequel des nombreux types possibles il veut cette fois-ci.