Problème avec des variants polymorphes + modules en OCaml

Bonjour,

Ce post est à peu près mon dernier espoir avant d’envoyer un mail sur la ML d’OCaml en espérant que je puisse trouver une réponse positive à mon problème.

Mon problème vient d’une idée toute bête, mais est basée sur le $\lambda$-calcul : comment implémenter un $\lambda$-calcul simple et non typé, qui si je l’étends par exemple avec les constructeurs du produit, je puisse réutiliser un maximum l’implémentation que j’ai de mon $\lambda$-calcul simple.

La solution que j’ai pour le moment est la suivante :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12

type 'a _t = [`App of 'a * 'a | `Lam of ('a -> 'a)]

type t = t _t

let rec step (t:[> `App of 'a * 'a | `Lam of ('a -> 'a)]) (k:'a -> 'a) : 'a =
  match t with
  | `App(`Lam f, x) -> f x
  | `App(t,u) -> `App(step t k, step u k)
  | `Lam f -> `Lam f
  | _ -> k t

let view_step : t -> t = fun t -> step t (fun x -> assert false)

On se donne un type polymorphe _t qu’on implémente par des variants polymorphes afin de l’étendre ensuite. Notre vrai type pour notre $\lambda$-calcul sera t. Sans variants polymorphes, l’implémentation de t rquiert d’utiliser l’option rectypes du compilateur mais avec les variants polymorphes, l’option semble être automatique.

Ensuite, on se donne une fonction step qui calcule une étape de $\beta$-reduction avec une stratégie similaire à celle d’OCaml (on ne réduit pas sous les abstractions).

Afin de pouvoir l’étendre par la suite, notre fonction prend une fonction qui sera appelée pour les constructeurs qu’elle ne sait pas traiter.

Si on souhaite une fonction step juste pour notre simple langage, on peut remplacer k par un assert false.

Ensuite, on peut étendre notre langage avec des produits de la façon suivante :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

type 'a _u = ['a _t | `Fst of 'a  | `Snd of 'a | `Prod of 'a * 'a]

type u = u _u

let rec step' t k =
  match t with
  | `Fst (`Prod(l,r)) -> step' l k
  | `Snd (`Prod(l,r)) -> step' r k
  | `Fst t ->
    begin
      match step' t k with
      | `Prod(t,u) -> t
      | _ as t-> `Fst t
    end
  | `Snd t ->
    begin
      match step' t k with
      | `Prod(t,u) -> t
      | _ as t-> `Fst t
    end
  | `Lam _ | `App _ as t-> step t (fun x -> step' x k)
  | _ -> k t

let view_step' : u -> u = fun t -> step' t (fun x -> assert false)

Pour le moment, les types sont inutiles en fait, pour le moment ils sont là seulement à titre d’indication. Mon problème est le suivant : J’aimerai écrire la signature de module suivante (la signature n’est pas fixe) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15

module type View =
sig
  type view

  val step : view -> view
end

module type Sig =
sig
  type 'a t

  val step : 'a t -> ('a -> 'a) -> 'a

  module View:View
end

De telle sorte à ce que je puisse encapsuler notre premier calcul dans un module de type Sig, et le second dans un foncteur de type Sig -> Sig.

La question est donc la suivante : est-il possible d’écrire la signature du module Sig ?

Avec la signature que j’ai donnée plus haut, OCaml se plaint car le type de step n’est pas bon :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16

Error: Signature mismatch:
       Modules do not match:
         sig
           type 'a t = [ `App of 'a * 'a | `Lam of 'a -> 'a ]
           val step :
             ([> `App of 'a * 'a | `Lam of 'a -> 'a ] as 'a) ->
             ('a -> 'a) -> 'a
         end
       is not included in
         Sig
       Values do not match:
         val step :
           ([> `App of 'a * 'a | `Lam of 'a -> 'a ] as 'a) ->
           ('a -> 'a) -> 'a
       is not included in
         val step : 'a t -> ('a -> 'a) -> 'a

En fait, j’aimerai indiqué à OCaml que la fonction puisse prendre au moins du ’a t :

1
2
3
4
5
6
7
8

module type Sig =
sig
  type 'a t

  val step : [>'a t] -> ('a -> 'a) -> 'a

  module View:View
end

Mais ce n’est pas permi car il ne sait pas que 'a t est un variant polymorphe. Et je ne souhaite pas expliciter le type de 'a t sinon je ne peux pas avoir un foncteur pour le produit par exemple.

Je suis à l’écoute de toutes vos solutions, y compris changer initialement mes types tant que je peux avoir une signature Sig qui représente ma théorie de base et rajouter le produit serait un foncteur en OCaml de Sig -> Sig.

Salut,

Ça n’est pas très lié à ton problème mais si on ajoute des Fst, Snd et Pair au 𝜆-calcul non typé (surjective paring), on obtient un système non confluent (cf. ça).

Je ne connais pas l’OCaml mais ça ne fonctionne pas en faisant sans ce subtyping ? On fait step t step au lieu de step t (fun x -> assert false) (dans la fonction step on supprime le dernier pattern et on appelle k récursivement pour App) et avec ce qui suit.

1

type 'a _u = [`Normal of ('a _t) | `Fst of 'a  | `Snd of 'a | `Prod of 'a * 'a]

Il doit exister une théorisation propre de ce genre de fonction récursive, je me souviens de quelque chose comme ça que j’essaierai de retrouver.

Par contre il n’y a pas un problème avec le type du retour de step ? Je ne suis pas convaincu de cette manière de faire même sans ajouter les produits.

Une question comme ça : est-ce qu’on peut modéliser le 𝜆-calcul non typé par juste le type récursif type t = t -> t ? Je dis ça parce qu’un modèle du 𝜆-calcul non typé, c’est dans une catégorie cartésienne fermée un objet $U$ avec un isomorphisme $U ≅ U^U$ (ou seulement une rétraction de $U$ sur $U^U$ si on ne veut pas la 𝜂-expansion).

Salut,

Ça n’est pas très lié à ton problème mais si on ajoute des Fst, Snd et Pair au 𝜆-calcul non typé (surjective paring), on obtient un système non confluent (cf. ça).

Intéressant, cependant dans ma formulation, je n’ai pas ces règles pour l’eta-expansion du produit.

Je ne connais pas l’OCaml mais ça ne fonctionne pas en faisant sans ce subtyping ? On fait step t step au lieu de step t (fun x -> assert false) (dans la fonction step on supprime le dernier pattern et on appelle k récursivement pour App) et avec ce qui suit.

1	type 'a _u = [`Normal of ('a _t) | `Fst of 'a | `Snd of 'a | `Prod of 'a * 'a]

Si je comprends bien ton idée, tu vas avoir un soucis car la première fonction step ne sait traiter que les constructeurs App et Lam. Comment réutiliser cette fonction pour qu’elle puisse traiter les cas ’Fst’, ’Snd’ … ?

Mais je dois pas trop comprendre ton idée, car je vois pas l’avantage d’utiliser un constructeur Normal.

Il doit exister une théorisation propre de ce genre de fonction récursive, je me souviens de quelque chose comme ça que j’essaierai de retrouver.

Oh, si tu as un lien, je suis preneur  !

Par contre il n’y a pas un problème avec le type du retour de step ? Je ne suis pas convaincu de cette manière de faire même sans ajouter les produits.

Peut-être. Le fait que l’intention c’est d’utiliser step avec un type 'a t tel que 'a t = 'a fait que je me suis probablement emmelé les pinceaux.

J’ai l’impression :

1
2
3
4
5

type t = t -> t

let omega x = x x

let omega2 = omega omega

Il faut activer l’option -rectypes cependant.

Mais je dois pas trop comprendre ton idée, car je vois pas l’avantage d’utiliser un constructeur Normal.

J’ai peut-être mélangé plusieurs trucs dans ce que j’ai raconté… Un truc qui ne s’applique pas ici est le suivant. Il faut qu’on ait un type paramétrique t(x) qui soit fonctoriel en x (ie une fonction x->y donne une fonction t(x)->t(y), ce n’est pas le cas ici). Soit t^∞ ≔ t(t^∞). Alors une fonction t(v) -> v donne une fonction t^∞ -> v. C’est la notion de catamorphisme (généralisation de fold).

Ensuite si on définit u(x) comme étant t(x) + p(x) avec un certain p(x), et si on a déjà défini une fonction t(v) -> v, alors on n’a plus qu’à définir la partie p(v) -> v pour avoir une fonction u(v) -> v et donc une fonction u^∞ -> v.

Le Normal apportait juste que si on avait plein de constructeurs pour _t, ça les groupe tous et on peut réutiliser step sans se servir du sous-typage. Mais pour éliminer le sous-typage il faut aussi gérer le fait que la récursion se fait sur deux niveaux, peut-être en mettant un ('a _t) _t dans le type de step mais bref c’est bancal.

Puis j’ai mélangé ça avec une autre idée (rapidement, si on a une fonction (v->v) -> (t(v) -> t(v)), on peut prendre v=t^∞ et on obtient (t^∞ -> t^∞) -> (t^∞ -> t^∞), puis on prend un point fixe de ça pour obtenir quelque chose de défini récursivement).

Peut-être. Le fait que l’intention c’est d’utiliser step avec un type 'a t tel que 'a t = 'a fait que je me suis probablement emmelé les pinceaux.

Oui, je n’avais pas compris ça.

Mais je ne vois pas ce que le foncteur que tu veux définir est censé faire en général, sans parler de OCaml. On part d’un type a tel que a _t = a et d’une fonction a _t -> (a->a) -> a, et on doit produire un type b tel que b _u = b et une fonction b _u -> (b->b) -> b, c’est ça ? Mais que doit satisfaire cette fonction par rapport à celle dont on part, de manière générale ?

Oh, si tu as un lien, je suis preneur  !

Désolé, je ne me souviens pas très bien. Je crois que ce à quoi je pensais est le genre de choses qu’on trouve en cherchant "scrap your boilerplate". Voir ici. Si ça se trouve ça n’a rien à voir avec le sujet mais j’ai pas le temps de vérifier.

Et aussi je ne vois pas ce que tu veux faire avec ça au final. Avec juste type t = t->t, on ne peut pas faire grand chose (on ne peut pas afficher les termes, chercher des forme normale pour les comparer, rien à part construire des termes). Avec ce que tu fais j’ai l’impression que c’est pareil.