Comment se rapporter au type à partir du contexte extérieur

Question

Considérons l'extrait de code suivant :

blah :: a -> b -> a
blah x y = ble x where
    ble :: b -> b
    ble x = x

Cela compile bien sous GHC, ce qui signifie essentiellement que b de la 3ème ligne est différent de b de la première ligne.

Ma question est simple : existe-t-il un moyen d'établir une relation entre la déclaration de type de l'utilisateur et la déclaration de type de l'utilisateur ? ble à un type utilisé dans un contexte externe, c'est-à-dire la déclaration de type de blah ?

Évidemment, il ne s'agit que d'un exemple et non d'un cas réel d'utilisation des déclarations de type.

Answer 1

Cela est possible avec le ScopedTypeVariables extension. Vous devez utiliser des forall explicites pour faire entrer les variables de type dans la portée.

blah :: forall a b. a -> b -> a
blah x y = ble x where
    ble :: b -> b
    ble x = x

Essayer de charger cette définition avec ScopedTypeVariables activé donne :

foo.hs:2:16:
    Couldn't match type `a' with `b'
      `a' is a rigid type variable bound by
          the type signature for blah :: a -> b -> a at foo.hs:2:1
      `b' is a rigid type variable bound by
          the type signature for blah :: a -> b -> a at foo.hs:2:1
    In the first argument of `ble', namely `x'
    In the expression: ble x
    In an equation for `blah':
        blah x y
          = ble x
          where
              ble :: b -> b
              ble x = x

Vous pouvez dire que GHC interprète les deux b comme le même type parce que l'erreur dit que a et b sont liés sur la même ligne.

Answer 2

Si vous ne voulez pas utiliser les ScopedTypeVariables, vous pouvez utiliser les bonnes vieilles méthodes suivantes asTypeOf fonction.

-- defined in Prelude
asTypeOf :: a -> a -> a
x `asTypeOf` y = x

---

blah :: a -> b -> a
blah x y = ble x where
    ble x = x `asTypeOf` y

Bien sûr, cela ne compilera pas à cause de l'erreur de type.

Mise à jour :

Je tiens à souligner que, parfois, il faut être un peu rusé pour faire ce que l'on veut avec asTypeOf . Prenons l'exemple suivant qui utilise de manière superflue asTypeOf parce que je ne veux pas penser à un cas qui a réellement besoin asTypeOf . Des solutions similaires fonctionneraient de la même manière dans des cas réels.

foo :: Bounded a => Maybe a -> a
foo m = x
  where
    x = maxBound -- Q: how do I make (x :: a) when given (Maybe a)?
    _ = Just x `asTypeof` m -- A: witchcraft!