Skip to content

Commit

Permalink
Migrate /capsule to xvw.lol
Browse files Browse the repository at this point in the history
  • Loading branch information
xvw committed Nov 14, 2022
1 parent 581c6de commit 5fb2767
Show file tree
Hide file tree
Showing 10 changed files with 450 additions and 273 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/pfioooouuuu.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ jobs:
uses: peaceiris/actions-gh-pages@v3
with:
deploy_key: ${{ secrets.ACTIONS_DEPLOY_KEY }}
publish_dir: ./www/capsule
publish_dir: ./www
external_repository: xvw/xvw.github.io
publish_branch: master
enable_jekyll: false
2 changes: 1 addition & 1 deletion content/bars.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,5 +24,5 @@ indexes:
fréquenter à Bruxelles !
links:
- name: Ethylo
href: /capsule/pages/ethylo.html
href: /pages/ethylo.html
---
4 changes: 2 additions & 2 deletions content/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,15 +18,15 @@ indexes:
synopsis: Notes plus-ou-moins organisées relatives à la programmation.
links:
- name: Bribes & Encodages
href: /capsule/tricks.html
href: /tricks.html
- name: Adresses
synopsis:
Comme il est compliqué d'être productif quand on est monomaniaque, j'essaie de
diversifier mes sujets de rédactions en documentant les adresses que j'apprécie
dans les quelques villes que je visite.
links:
- name: Bars et cafés
href: /capsule/bars.html
href: /bars.html
---

Vous me trouverez sur [Mastodon](https://merveilles.town/@xvw), sur
Expand Down
6 changes: 3 additions & 3 deletions content/pages/ethylo.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,16 +19,16 @@ tags:
- schaerbeek
breadcrumb:
- name: Bars et cafés
href: /capsule/bars.html
href: /bars.html
- name: Bruxelles
href: /capsule/bars.html#index-bruxelles
href: /bars.html#index-bruxelles
---

> Comme toute rencontre démarre souvent de zéro (ou de _rien_, pour certains,
> c'est la même chose), j'ai rencontré Romain en 2009. À l'époque, nous étions
> étudiants, dans une école d'informatique de gestion et nous étions aussi,
> _approximativement_ voisins, nous étions
> [fringants](/capsule/images/romain-xavier.jpg) On peut dire que nos
> [fringants](/images/romain-xavier.jpg) On peut dire que nos
> expérimentations mixologiques ont commencé rapidement... mais avec bien peu
> d'ambition (géneralement deux ingrédients). Rapidement, la lourdeur de la
> formation nous fit nous réorienter. Je me dirigeai vers l'informatique théorique
Expand Down
59 changes: 28 additions & 31 deletions content/pages/oop-refl.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
---
title: Méthodes gardées
creation_date: 2022-05-29
description:
description:
Implémentation de "méthodes gardées" en utilisant des témoins d'égalités
de types.
synopsis:
Les **méthodes gardées** permettent d'attacher des **contraintes**
au receveur (`self`) **uniquement pour certaines méthodes**, permettant
donc de n'appeler ces méthodes que si le receveur satisfait ces contraintes
(ces _guards_). [OCaml](https://ocaml.org) ne permet pas, syntaxiquement,
de définir _directement_ ce genre de méthodes. Dans cette note, nous allons
synopsis: Les **méthodes gardées** permettent d'attacher des **contraintes**
au receveur (`self`) **uniquement pour certaines méthodes**, permettant
donc de n'appeler ces méthodes que si le receveur satisfait ces contraintes
(ces _guards_). [OCaml](https://ocaml.org) ne permet pas, syntaxiquement,
de définir _directement_ ce genre de méthodes. Dans cette note, nous allons
voir comment les encoder en utilisant un **témoin d'égalité de type**.
tags:
- programmation
Expand All @@ -19,7 +18,7 @@ tags:
- gadt
breadcrumb:
- name: Bribes & Encodages
href: /capsule/tricks.html#index-ocaml
href: /tricks.html#index-ocaml
---

Les _défenseurs_ de la **programmation orientée objets** défendent souvent cette
Expand All @@ -35,7 +34,6 @@ Dans les critiques formulées, nous allons nous intéresser tout particulièreme
l'orienté objets, car il serait envisageable de les intégrer, mais qui manque
dans beaucoup de langages OOP populaires.


## Présentation du problème

Quand un langage (dont les vérification des types est effectuée avant
Expand All @@ -51,7 +49,7 @@ On rend `MyClass` générique en admettant que la variable de type `T` est un
sous-type de `S`. Le problème est que la contrainte agit **sur toute la
classe**. Pourtant, parfois, nous voudrions pouvoir n'avoir des contraintes
que **sur certaines méthodes**. Par exemple, admettons que nous ayons une
classe `MyList` décrivant une liste:
classe `MyList` décrivant une liste:

```java
class MyList<A> extends ArrayList<A> {
Expand All @@ -60,6 +58,7 @@ class MyList<A> extends ArrayList<A> {
}
}
```

Comment décrire une méthode `flatten` qui pour une liste `[[1, 2, 3], [4, 5]]`
produirait la liste `[1, 2, 3, 4, 5]` ? Si on place la contrainte au niveau
de la classe on force notre liste à être "_tout le temps une liste de liste_"
Expand Down Expand Up @@ -138,21 +137,20 @@ classe** semble suffire), on corrige tous les soucis révélés précédemment:
- on ne casse pas l'envoi de messages réguliers
- on bénéficie toujours des membres disponnibles (donc on n'échappe pas de
représentations)

Même si les méthodes gardées semblent être nécéssaires, je ne connais
malheureusement pas de langages _mainstream_ qui permettent leur définition.
Voila qui est très triste. Heureusement, en OCaml, il est possible de les
_encoder_.


### La symétrie OOP/FP : théorie et pratique

Comme les méthodes gardées sont assez rares dans les langages de programmation
populaires j'ai découvert leur existence assez récemment, en lisant les
[transparents](http://gallium.inria.fr/~scherer/doc/oo-fp-symmetry-bob-2020.org)
de la présentation "_[The Object-Oriented/Functional-Programming symmetry: theory
and practice ](https://www.youtube.com/watch?v=TrameN7BTCQ)_" de [Gabriel
Scherer](http://gallium.inria.fr/~scherer/).
Scherer](http://gallium.inria.fr/~scherer/).

Je recommande cette présentation qui présente une **symétrie** entre les outils
de la programmation fonctionnelle statiquement typée et la programmation
Expand All @@ -163,7 +161,7 @@ Malheureusement non couvertes pendant la présentation (_le temps est souvent
l'ennemi d'un présentateur_), toute une section est dédiée aux méthodes gardées
dans les transparents. L'exemple original propose une observation symétrique
entre l'implémentation de la fonction `flatten` dans un style fonctionnel
classique :
classique :

```ocaml
type 'a list = ...
Expand Down Expand Up @@ -197,8 +195,8 @@ method flatten : 'b olist with 'a = 'b olist
Cette syntaxe permet de décrire une méthode gardée et pourrait se généraliser de
cette manière : `method method_name : return_type with generic_type = other_type`.
Un peu à la manière des **substitution** dans les modules, on pourrait décrire
des contraintes sur plusieurs génériques au moyen de `and`. Par exemple :
`method foo : string with 'a = string and b = int` pour une classe paramétrée
des contraintes sur plusieurs génériques au moyen de `and`. Par exemple :
`method foo : string with 'a = string and b = int` pour une classe paramétrée
par deux types : `class ['a, 'b] t`.

En complément, cette syntaxe permettrait aussi de définir des comportements spécifiques
Expand Down Expand Up @@ -229,7 +227,7 @@ au moyen de quelques petits outils.
> de batterie midi, donc en cherchant son pseudonyme sur _Google_, j'ai tout de
> suite eu, dans les suggestions: `octachron ocaml`.)
Notre objectif est de permettre d'ajouter une contrainte à certaines méthodes pour
Notre objectif est de permettre d'ajouter une contrainte à certaines méthodes pour
ne les rendres accessibles que si le type du receveur la satisfait. Sans passer par
de la modification syntaxique du langage, modeliser une contrainte peut **consister
à donner un paramètre additionnel qui l'enforce**. En d'autres mots, on voudrait
Expand All @@ -243,14 +241,14 @@ dans le langage, il existe une manière assez directe de définir un témoins
d'égalité de types:

```ocaml
type (_, _) eq =
type (_, _) eq =
| Refl : ('a, 'a) eq
```

Le type `eq`, qui n'a qu'un seul constructeur: `Refl`, et permet de représenter
des égalité de types **non connues par le _type-checker_**. Comme on ne peut que
construire des valeurs `Refl` qui associent deux types égaux, l'instanciation
de `Refl` dans un _scope_ garantit qu'ils sont équivalent. Par exemple :
de `Refl` dans un _scope_ garantit qu'ils sont équivalent. Par exemple :

```ocaml
type other_int = int
Expand All @@ -266,14 +264,14 @@ un type ou encore quand la représentation du type est cachée par l'abstraction

L'objectif de cette note n'est pas de nous étendre sur `eq` donc ne retenons que
le fait que si on peut construire une valeur `Refl`, on peut avoir une garantie
que deux types _syntaxiquement différents_ sont en fait égaux.
que deux types _syntaxiquement différents_ sont en fait égaux.

### Contraindre avec `eq`

Reprenons notre exemple qui fournit une API objet à une liste. Voici son interface:

```ocaml
class type ['a] obj_list =
class type ['a] obj_list =
object ('self)
method length : int
method append : 'a list -> 'a obj_list
Expand All @@ -284,8 +282,7 @@ class type ['a] obj_list =

Pour donner un type à `flatten`, ou voudrait imposer que `'a` (le paramètre de
type de la classe `obj_list`) soit une liste. En d'autre mot, nous voudrions
**une preuve que `'a` est de type `'b list`**. Soit garantir que `'a` et `'b
list`, bien que syntaxiquement différents, soient égaux. Rien de plus simple,
**une preuve que `'a` est de type `'b list`**. Soit garantir que `'a` et `'b list`, bien que syntaxiquement différents, soient égaux. Rien de plus simple,
il suffit de demander d'en fournir une valeur de type `('a, 'b list) eq`:

```ocaml
Expand All @@ -294,7 +291,7 @@ method flatten : ('a, 'b list) eq -> 'b list

Maintenant que nous avons une interface qui décrit une liste avec une méthode
`flatten` qui contraint le receveur à être `une liste de quelque chose`,
implémentons concrètement une classe qui implémente `obj_list`.
implémentons concrètement une classe qui implémente `obj_list`.

#### Implémentation de l'interface `obj_list`

Expand All @@ -308,13 +305,13 @@ let my_list (list : 'a list) =
method length = List.length l
method append x = {<l = List.append l x>}
method uncons = match l with [] -> None | x :: xs -> Some (x, {<l = xs>})
method flatten = ???
end
```

Maintenant, intéressons-nous à `flatten`. On va récursivement parcourir
la liste en concaténant chaque élément au précédent. Par exemple :
la liste en concaténant chaque élément au précédent. Par exemple :
`[[1]; [2]; [3]]` donnera `[1] @ [2]; [3]`. Au delà des annotations un
peu bruyante, toute l'astuce réside dans l'instanciation de `Refl` pour
nous fournir une évidence sur le fait que `'a = 'b list`.
Expand All @@ -336,11 +333,11 @@ method flatten : 'b. ('a, 'b list) eq -> 'b list =
Maintenant que nous sommes capable de contraindre certaines méthodes, essayons
d'ajouter une méthode `sum` qui produit la somme d'une liste d'entiers !
Premièrement ajoutons `sum` à notre interface. Cette fois, on veut contraindre
notre paramètre de type à être `int`. Pour cela, il suffit de prendre
notre paramètre de type à être `int`. Pour cela, il suffit de prendre
`('a, int) eq` comme témoin d'égalité:

```ocaml
class type ['a] obj_list =
class type ['a] obj_list =
object ('self)
method length : int
method append : 'a list -> 'a obj_list
Expand All @@ -355,7 +352,7 @@ de la fonction `fold_left`.

```ocaml
method sum : ('a, int) eq -> int =
let aux : type a. a list -> (a, int) eq -> int = fun list Refl ->
let aux : type a. a list -> (a, int) eq -> int = fun list Refl ->
List.fold_left (fun acc x -> acc + x) 0 list
in aux l
```
Expand Down Expand Up @@ -405,8 +402,8 @@ fournit _implicitement_, allégant ainsi l'appel, n'obligeant pas l'utilisateur
fournir manuellement `Refl`.

Même si l'encodage est un peu lourd, et que l'on pourrait imaginer un support
natif dans le langage pour simplifier la définition de méthode gardée,
natif dans le langage pour simplifier la définition de méthode gardée,
**manipuler explicitement un témoin d'égalité de type permet de les encoder**.
Est-ce utile ? Comme la programmation OOP est rarement encouragée en OCaml,
Est-ce utile ? Comme la programmation OOP est rarement encouragée en OCaml,
_probablement pas_, mais c'était tout de même amusant de présenter un cas
d'usages concret et pratique à l'utilisation de témoins d'égalités !
22 changes: 10 additions & 12 deletions content/tricks.md
Original file line number Diff line number Diff line change
@@ -1,22 +1,20 @@
---
title: Bribes & Encodages
description: Bribes, encodages et curiosités en programmation
synopsis:
En programmation, il existe parfois plusieurs manière de résoudre
des problème (_ou d'en créer_). Cette page indexe des petits
fragments de code ou des ruses de **sioux** qui _solutionnent_ des
problèmes (_qui parfois n'en sont pas_). Ce n'est pas toujours très
utile aux premiers abords, mais je trouve ça parfois intéressant.
synopsis: En programmation, il existe parfois plusieurs manière de résoudre
des problème (_ou d'en créer_). Cette page indexe des petits
fragments de code ou des ruses de **sioux** qui _solutionnent_ des
problèmes (_qui parfois n'en sont pas_). Ce n'est pas toujours très
utile aux premiers abords, mais je trouve ça parfois intéressant.
tags:
- programmation
- type
- ocaml
- programmation
- type
- ocaml
toc: false
indexes:
- name: OCaml
synopsis:
Bribes et encodages utilisant le langage OCaml.
synopsis: Bribes et encodages utilisant le langage OCaml.
links:
- name: Méthodes gardées
href: /capsule/pages/oop-refl.html
href: /pages/oop-refl.html
---
Loading

0 comments on commit 5fb2767

Please sign in to comment.