Avoir un `(a -> b) -> b` équivaut-il à avoir un` a`?

Question

Dans un langage purement fonctionnel, la seule chose que vous pouvez faire avec une valeur, c'est d'appliquer une fonction à elle.

En d'autres termes, si vous voulez faire quelque chose d'intéressant avec une valeur de type a vous avez besoin d'une fonction (par exemple) avec le type f :: a -> b puis de l'appliquer. Si quelqu'un vous remet (flip apply) a type (a -> b) -> b, c'est qu'un substitut approprié pour a?

Et que feriez-vous appel à quelque chose de type (a -> b) -> b? Voyant que cela semble être un stand-in pour un a,, je serais tenté de l'appeler un proxy, ou quelque chose de http://www.thesaurus.com/browse/proxy.

Answer 1

luqui la réponse est excellente, mais je vais vous donner une autre explication de l' forall b. (a -> b) -> b === a pour un couple de raisons: d'Abord, parce que je pense que la généralisation de Codensity est un peu overenthusiastic. Et deuxièmement, parce que c'est une occasion de lier un tas de choses intéressantes ensemble. À partir de!

z5h de la Boîte Magique

Imaginez que quelqu'un a renversé une pièce de monnaie puis le mettre dans une boîte magique. Vous ne pouvez pas voir à l'intérieur de la boîte, mais si vous choisissez un type b et passe de la boîte une fonction du type Bool -> b, la boîte va cracher un b. Que pouvons-nous apprendre au sujet de cette zone, sans regarder à l'intérieur? Peut-on savoir quel est l'état de la pièce est? Pouvons-nous apprendre de ce mécanisme de la boîte utilise pour produire de l' b? Comme il s'avère, nous pouvons faire les deux.

Nous pouvons définir la zone de rang 2 et la fonction de type Box Bool où

type Box a = forall b. (a -> b) -> b

(Ici, le rang 2 de type signifie que la case maker choisit a , et la boîte utilisateur choisit b.)

Nous avons mis l' a dans la zone et puis on ferme la boîte, de la création... d'une fermeture.

-- Put the a in the box.
box :: a -> Box a
box a f = f a

Par exemple, box True. L'application partielle est juste un moyen astucieux pour créer des fermetures!

Maintenant, c'est la pièce à pile ou face? Depuis que j', la boîte de l'utilisateur, je suis autorisé à choisir l' b, je peux choisir Bool et passer dans une fonction, Bool -> Bool. Si je décide id :: Bool -> Bool alors la question est: est-ce la boîte de cracher sur la valeur qu'elle contient? La réponse est que la boîte soit cracher à la valeur qu'il contient ou qu'il va cracher non-sens (d'une valeur inférieure comme undefined). En d'autres termes, si vous obtenez une réponse alors que la réponse doit être correcte.

-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id

Parce que nous ne pouvons pas générer des valeurs arbitraires en Haskell, la seule chose que le sens de la boîte peut faire, c'est d'appliquer la fonction donnée de la valeur, il se cache. C'est une conséquence de polymorphisme paramétrique, aussi connu comme parametricity.

Maintenant, pour montrer qu' Box a est isomorphe a' a, nous avons besoin de prouver deux choses à propos du boxing et unboxing. Nous devons prouver que vous obtenez ce que vous mettez dans et que vous pouvez mettre dans ce que vous sortez.

unbox . box = id
box . unbox = id

Je vais le faire à la première, et laisser la seconde comme un exercice pour le lecteur.

  unbox . box
= {- definition of (.) -}
  \b -> unbox (box b)
= {- definition of unbox and (f a) b = f a b -}
  \b -> box b id
= {- definition of box -}
  \b -> id b
= {- definition of id -}
  \b -> b
= {- definition of id, backwards -}
  id

(Si ces preuves semblent plutôt trivial, c'est parce que tous (total) fonctions polymorphes en Haskell sont les transformations naturelles et de ce que nous sommes en train de prouver ici est de naturalité. Parametricity encore une fois, nous offre, avec les théorèmes de bas, à bas prix!)

Comme d'un côté et d'un autre exercice pour le lecteur, pourquoi je ne peux pas définir réellement rebox avec (.)?

rebox = box . unbox

Pourquoi dois-je incorporer la définition de l' (.) moi-même, comme une sorte de caverne de la personne?

rebox :: Box a -> Box a
rebox f = box (unbox f)

(Astuce: quels sont les types d' box, unbox, et (.)?)

Identité et Codensity et de Yoneda, Oh Mon dieu!

Maintenant, comment peut-on généraliser Box? luqui utilise Codensity: les deux bs sont généralisées par l'arbitraire d'un constructeur de type que nous appellerons f. C'est le Codensity de transformation de l' f a.

type CodenseBox f a = forall b. (a -> f b) -> f b

Si nous fixons f ~ Identity puis nous revenons Box. Cependant, il existe une autre option: on peut frapper seulement le type de retour avec f:

type YonedaBox f a = forall b. (a -> b) -> f b

(J'ai sorte de donné du jeu ici avec ce nom, mais nous allons y revenir.) Nous pouvons également fixer f ~ Identity ici pour récupérer Box, mais nous laissez la boîte de l'utilisateur de passer dans une fonction normale plutôt qu'une Kleisli flèche. Pour comprendre ce que nous sommes généraliser, revenons sur la définition de l' box:

box a f = f a

Eh bien, c'est juste flip ($), n'est-ce pas? Et il s'avère que nos deux autres cases sont construites par la généralisation ($): CodenseBox est appliquée partiellement, renversé monadique lier et YonedaBox est appliquée partiellement flip fmap. (Cela explique aussi pourquoi, Codensity f est Monad et Yoneda f est Functor pour tout choix d' f: La seule façon de créer l'on est par la fermeture de plus d'un bind ou fmap, respectivement.) En outre, ces deux ésotérique de la catégorie de la théorie des concepts sont vraiment des généralisations d'un concept qui est familier à beaucoup de travail programmeurs: le CPS transformer!

En d'autres termes, YonedaBox est le Yoneda d'Incorporation et de l'correctement captée box/unbox lois pour YonedaBox sont la preuve du Lemme de Yoneda!

TL;DR:

forall b. (a -> b) -> b === a est une instance de la Lemme de Yoneda.

Answer 2

Cette question est une fenêtre sur un certain nombre de la plus profonde des concepts.

Tout d'abord, notez qu'il existe une ambiguïté dans cette question. Entendons-nous le type forall b. (a -> b) -> b, ce qui nous permet d'instancier b avec quel que soit le type que nous aimons, ou voulons-nous dire (a -> b) -> b de b que nous ne pouvons pas choisir.

On peut formaliser cette distinction en Haskell ainsi:

newtype Cont b a = Cont ((a -> b) -> b)
newtype Cod a    = Cod (forall b. (a -> b) -> b)

Ici, nous voyons un peu de vocabulaire. Le premier type est l' Cont monade, la deuxième est CodensityIdentity, bien que ma familiarité avec le dernier terme n'est pas assez fort pour dire ce que vous devez appeler que en anglais.

Cont b a ne peut pas être équivalent à a moins a -> b peut contenir au moins autant d'information qu' a (voir Dan Robertson commentaire ci-dessous). Ainsi, par exemple, notez que vous ne pouvez jamais obtenir quoi que ce soit d' ContVoida.

Cod a est équivalent à a. Pour voir cela, il suffit de témoin de l'isomorphisme:

toCod :: a -> Cod a
fromCod :: Cod a -> a

dont les implémentations, je vais le laisser comme un exercice. Si vous voulez vraiment le faire, vous pouvez essayer de prouver que cette paire est vraiment un isomorphisme. fromCod . toCod = id est facile, mais toCod . fromCod = id nécessite le libre théorème de Cod.

Answer 3

Les autres réponses ont fait un excellent travail décrivant la relation entre les types d' forall b . (a -> b) -> b et a mais je tiens à souligner une mise en garde, car elle conduit à de très intéressantes questions ouvertes qui j'ai travaillé.

Techniquement, forall b . (a -> b) -> b et a sont pas isomorphe dans une langue comme Haskell qui (1) permet d'écrire une expression qui n'a pas de fin et de (2) est soit en appel par valeur (strict) ou contient seq. Mon point ici est de ne pas être tâtillon ou de montrer que parametricity est affaibli en Haskell (comme c'est bien connu), mais qu'il peut être soigné moyens de la renforcer et, dans un certain sens récupérer isomorphisms comme celui-ci.

Il y a des termes de type forall b . (a -> b) -> b qui ne peuvent pas être exprimées en a. Pour comprendre pourquoi, nous allons commencer par regarder la preuve Rein gauche comme un exercice, box . unbox = id. Il s'avère que cette preuve est en fait plus intéressant que celui de sa réponse, car elle repose sur parametricity de manière cruciale.

box . unbox
= {- definition of (.) -}
  \m -> box (unbox m)
= {- definition of box -}
  \m f -> f (unbox m)
= {- definition of unbox -}
  \m f -> f (m id)
= {- free theorem: f (m id) = m f -}
  \m f -> m f
= {- eta: (\f -> m f) = m -}
  \m -> m
= {- definition of id, backwards -}
  id

La démarche intéressante, où parametricity arrive en jeu, est l'application de la libre théorème f (m id) = m f. Cette propriété est une conséquence de l' forall b . (a -> b) -> b, le type d' m. Si nous pensons m comme une boîte avec une valeur sous-jacente de type a à l'intérieur, la seule chose m peut faire avec son argument est de l'appliquer à cette valeur sous-jacente et de retourner le résultat. Sur le côté gauche, cela signifie qu' f (m id) extraits de la valeur sous-jacente de la boîte, et le transmet f. Sur la droite, cela signifie qu' m s'applique f directement à la valeur sous-jacente.

Malheureusement, ce raisonnement n'est pas tout à fait tenir quand nous avons des termes tels que l' m et f ci-dessous.

m :: (Bool -> b) -> b
m k = seq (k true) (k false)

f :: Bool -> Int
f x = if x then ⊥ else 2`

Rappel, nous avons voulu montrer f (m id) = m f

f (m id)
= {- definition f -}
  if (m id) then ⊥ else 2
= {- definition of m -}
  if (seq (id true) (id false)) then ⊥ else 2
= {- definition of id -}
  if (seq true (id false)) then ⊥ else 2
= {- definition of seq -}
  if (id false) then ⊥ else 2
= {- definition of id -}
  if false then ⊥ else 2
= {- definition of if -}
  2

m f
= {- definition of m -}
  seq (f true) (f false)
= {- definition of f -}
  seq (if true then ⊥ else 2) (f false)
= {- definition of if -}
  seq ⊥ (f false)
= {- definition of seq -}
  ⊥

Clairement 2 n'est pas égal à ⊥ nous avons donc perdu notre gratuit théorème et l'isomorphisme entre a et (a -> b) -> b avec elle. Mais ce qui s'est passé, exactement? Essentiellement, m n'est pas seulement un bien comporté de la boîte, car il applique son argument à deux différentes valeurs sous-jacentes (et utilise seq pour assurer ces deux applications sont évalués), que l'on peut observer en passant dans une poursuite qui se termine sur l'une de ces valeurs sous-jacentes, mais pas les autres. En d'autres termes, m id = false n'est pas vraiment une représentation fidèle de l' m comme Bool parce qu'il 'oublie' le fait qu' m appelle son entrée avec les deux true et false.

Le problème est le résultat de l'interaction entre trois choses:

1. La présence de nontermination.
2. La présence de la seq.
3. Le fait que les termes de type forall b . (a -> b) -> b peuvent s'appliquer à leur entrée à plusieurs reprises.

Il n'y a pas beaucoup d'espoir d'obtenir des points 1 ou 2. Linéaire types peuvent nous donner une occasion de lutter contre la troisième question, bien que. Une fonction linéaire de type a ⊸ b est une fonction de type a type b qui doit utiliser son entrée exactement une fois. Si nous avons besoin d' m pour avoir le type forall b . (a -> b) ⊸ b, puis présente les règles de notre contre-exemple à la libre théorème et devrait nous montrer un isomorphisme entre a et forall b . (a -> b) ⊸ b , même en présence de nontermination et seq.

C'est vraiment cool! Il montre que la linéarité a la capacité de "sauver" des propriétés intéressantes par une meilleure maîtrise des effets qui peuvent faire de vrais général paramétré par un raisonnement difficile.

Une grande question demeure, cependant. Nous n'avons pas encore les techniques de prouver la libre théorème dont nous avons besoin pour le type forall b . (a -> b) ⊸ b. Il s'avère actuel des relations logiques (les outils que nous utilisons habituellement pour faire ces preuves) n'ont pas été conçus pour prendre en compte la linéarité de la manière qui est nécessaire. Ce problème a des conséquences pour l'établissement d'exactitude pour les compilateurs qui ne CPS traductions.