Re: Reason

Tu m'as un peu largué dans les types paramétriques.

Je dois avouer que je suis moi même perdu en essayant de comprendre ce que tu écris et ce que tu veux faire. Au départ, j'essayais de comprendre ce que tu voulais dire par : « les littéraux sont considérés différemment du type ». Veux-tu dire par là que les valeurs, comme 1, et les types, comme int, vivent dans des mondes différents ? Mais une telle situation est présente dans la quasi totalité des langages, à l'exception des langages avec types dépendants (comme Coq).

Ensuite tu as écrit : « Or a part dans fonctionnalité de généricité, le type n'est jamais une variable », et c'est là que j'ai explicité, à ma façon, ce que je comprenais d'une telle phrase; d'où mon texte sur les types paramétriques.

En OCaml, on peut définir une valeur comme un couple d'entier ainsi :

let i = (1, 2)

On peut également définir un alias du types des couples sous la forme d'un type paramétré ainsi :

type ('a, 'b) tuple = 'a * 'b

Ce type paramétré peut être vu comme une fonction des types dans les types à deux paramètres. La syntaxe Reason modifie la manière d'écrire de tels types en utilisant une syntaxe similaire à celle des fonctions :

type tuple 'a 'b = ('a, 'b)

Vois-tu l'analogie qu'il y a entre des fonctions entres valeurs et les types paramétriques (fonctions entre types) ?

let tuple a b = (a, b)

Ensuite viens la chose qui semble te déranger et que tu exprimes ainsi dans ton dernier message :

C'est ce mélange entre type de base et littéraux qui est impossible et très chiant en pratique.
[...]
L'idée de base est simplement d'ajouter un opérateur "est compatible avec le type de", je le notait '~' ou même '=' dans les définitions.

Ainsi, tu écris int ~ 1 ~ Name "a", pour définir un truc du nom de "a" qui est de type int et vaux 1.

Que veux tu faire ? Veux-tu que ton opérateur ~ ait comme premier paramètre un type (int dans ton exemple) et comme second paramètre une valeur de ce type (1 dans ton exemple) ? Ce qui fait de ton exemple, une autre manière d'écrire :

let (a : int) = 1

Mais si c'est bien ce que tu cherches à faire (avoir des fonctions qui prennent en paramètre aussi bien des types que des valeurs) alors tu cherches à avoir un système de types dépendants. Voici comment sont définies les listes polymorphes homogènes en Coq :

Inductive list (X:Type) : Type :=
 | nil : list X
 | cons : X -> list X -> list X.

Sur cette structure de donnée, on peut définir la fonction repeat ainsi :

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
 match count with
 | 0 => nil X
 | S count' => cons X x (repeat X x count')
 end.

Ici le premier paramètre de la fonction repeat est un type X, le second un terme x de type X et le troisième un terme count de type nat. On peut ainsi écrire :

Check repeat nat 4 5.
(* et coqide me répond :
 repeat nat 4 5
 : list nat
*)

Autrement dit on peut mélanger types et littéraux sans problèmes. Est-ce cela que tu veux ?

Tu me dis pourquoi se faire chier avec un système aussi compliqué ? Le coté formel permet plein de choses.

Je n'ai jamais dit « pourquoi se faire chier avec un système aussi compliqué ». Déjà, je ne considère pas Coq comme étant aussi compliqué qu'on veut bien le faire croire. C'est certes plus compliqué, mais aussi bien plus puissant, que OCaml mais sans être pour autant aussi complexe que sa réputation le laisse entendre. Enfin, au sujet des possibilités des approches formelles : tu prêches un convaincu ! La formalisation de la pensée, c'est synonyme de rigueur intellectuelle pour moi; et si c'est bien fait, alors effectivement cela ouvre de grandes possibilités.

Pour reprendre un de tes exemples

La où cela devient marrant, c'est si on introduit la négation. Genre int ~ (! 0), pour faire un entier qui n'est pas nulle.

le type des entiers non nuls se définie ainsi en Coq :

Definition non_nul := {n : nat | n <> 0}.

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.