Discussion :

[gg373]

Je me penche actuellement sur la quantification existentielle et j'avoue que je peine mais ça avance petit à petit. Il y a cependant une partie de l'article en.wikibooks.org>wiki>Haskell>Existentially_quantified_types où je n'ai rien capté du tout.

Je cite "La quantification universelle est utile pour définir des types de données qui ne sont pas déjà. Supposons que les paires n'existent pas en haskell. La quantification permettrait de les définir."

Et de suivre la définition suivante :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

newtype Pair a b = Pair (forall c. (a->b->c)->c)

Et pas d'autre explication. Ce type compile bien.
On voit que le contructeur attend un opérateur et renvoie une valeur de type universelle, donc rien de défini. Quelque chose dans le genre :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
uif :: (forall c. (Int -> Float -> c)->c)
uif op = undefined

Et effectivement,

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

p = Pair uif

passe très bien et je vérifie que ça ne ne fonctionne effectivement qu'avec un retour 'bottom' de uif étant donné le 'forall c.' imbriqué.
J'obtiens un type 'p :: Pair Int Float'
Tout ça est très beau, mais que faire de ce résultat ? En quoi on a défini l'équivalent d'un opérateur (,) même dans le monde des types et des EDSL ?

Si vous avez quelque lumière sémantique les amis.... Merci.

[Ptival]

De ce que je comprends, il veut faire ça :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
 
{-# LANGUAGE ExistentialQuantification, Rank2Types #-}
 
newtype Pair a b = Pair (forall c. (a -> b -> c) -> c)
 
pair :: a -> b -> Pair a b
pair x y = Pair (\f -> f x y)
 
pfst :: Pair a b -> a
pfst (Pair f) = f (\x y -> x)
 
psnd :: Pair a b -> b
psnd (Pair f) = f (\x y -> y)
 
main =
  do
    let p = pair 2 True
    print (pfst p)
    print (psnd p)

Je pense que c'est assez clair, demande si tu as besoin d'explications.

[Alp]

Et de suivre la définition suivante :

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

newtype Pair a b = Pair (forall c. (a->b->c)->c)

Et pas d'autre explication.

Je ne sais pas si tu as compris depuis, mais au cas où, je vais tenter de te donner l'intuition de "pourquoi c'est bien comme une paire".

Alors, regardons le type de plus près. On va juste se concentrer sur:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

forall c. (a -> b -> c) -> c

Il est important de voir qu'à ce point là de la définition, a et b sont déjà fixés, c'est "juste" des paramètres donnés à Pair. Pour encore moins se prendre la tête, on va même dire que a = Int et b = Float comme dans ton exemple.
Ca donne:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

forall c. (Int -> Float -> c) ->c

On voit que c'est le type d'une fonction. Comment une fonction peut être une paire? Techniquement, cette fonction n'est pas comme (,), évidemment.

Ce que le type nous dit par contre, c'est: "pour tout type c, si tu me donnes une fonction de type Int -> Float -> c, je te donne un c.

Sauf que ta valeur de type 'Pair Int Float' peut faire ça pour tout type c, cette seule et unique valeur de type Pair Int Float que t'as sous la main peut faire ça. Mais comment? On peut imaginer que ç'a un lien avec la fonction qu'elle prend en argument, mais il lui faudrait un Int et un Float pour pouvoir avoir un c, on est d'accord? Sinon, on pourrait faire marcher des idées pour des c bien particuliers, mais pas pour tous à la fois! Bah, avoir un Int et un Float, c'est pas ça une paire consistant d'un Int et un Float?

[SpiceGuid]

Ce que fais Ptival est une version typée du codage d'un couple en λ-calcul.

Ce que fais Alp c'est expliquer le produit dans une catégorie cartésienne (en français).

À ma connaissance il n'y a pas de 3ième façon de comprendre la chose.