## merd-devel — about merd development

You can subscribe to this list here.

 2000 2001 2002 2005 2006 2007 2008 2009 Jan Feb Mar Apr May Jun Jul Aug (5) Sep (43) Oct (15) Nov (20) Dec (2) Jan (12) Feb (20) Mar (7) Apr (18) May (23) Jun (4) Jul (2) Aug (19) Sep (3) Oct (19) Nov (27) Dec (23) Jan (2) Feb (16) Mar (18) Apr (16) May (24) Jun (2) Jul (3) Aug (1) Sep (16) Oct Nov Dec Jan Feb Mar Apr May Jun Jul Aug Sep Oct (1) Nov Dec (1) Jan Feb (2) Mar Apr May Jun Jul Aug (1) Sep (2) Oct (8) Nov Dec Jan (1) Feb Mar Apr May Jun Jul Aug Sep (1) Oct Nov Dec Jan Feb Mar Apr May Jun Jul Aug (1) Sep Oct Nov Dec Jan (1) Feb Mar Apr May Jun Jul Aug Sep Oct Nov Dec
S M T W T F S

1

2

3

4

5

6

7

8

9

10
(1)
11
(3)
12
(3)
13
(2)
14
(1)
15
(1)
16
(2)
17

18

19

20
(1)
21
(1)
22

23
(5)
24
(5)
25

26

27

28
(2)
29

30

Showing results of 27

1 2 > >> (Page 1 of 2)
 Re: [merd-devel] expression normalisation, more than covariance From: Pixel - 2001-11-28 19:27:09 ```Pixel writes: [...] > Question: in which case does c(a) | c(b) = c(a|b) holds? [...] > * AB > AB(a) = A(a) | B(a) > aka AB = A | B > > A(a) | A(b) => A(a|b) > AB(a) | AB(b) => is NOT AB(a|b) wrong: AB(a) | AB(b) = (A(a) | B(a)) | (A(b) | B(b)) = A(a) | A(b) | B(a) | B(b) = A(a|b) | B(a|b) = AB(a|b) > > > So in which case c(a) | c(b) => c(a|b) ?? > Well: > - if c is recursive (eg: List), it doesn't work (?) > => it doesn't work for List > - if c(a) = e1 | e2 | ... | en where only one ei use "a", it works wrong, make it: - if c(a) = e1 | e2 | ... | en where each ei use at most one "a" => it works for Maybe (Some use ony one "a", None use none) => it works for AB (both A and B use only one "a") so now, here is a wrong one: AA(a) = A(a,a) A(a,b) | A(c,d) => is NOT A(a|c, b|d) just like (a,b) | (c,d) is NOT (a|c, b|d) in fact A(a,b) | A(c,d) => A(a,b | c,d) ```
 [merd-devel] expression normalisation, more than covariance From: Pixel - 2001-11-28 01:12:11 ```Pb: is List(Int) | List(String) and List(Int | String) the same ? Answer: no, [ 1, "foo" ] is not a List(Int) | List(String) is a List(Int | String) Question: in which case does c(a) | c(b) = c(a|b) holds? * Maybe Maybe(a) = None | Some(a) aka Maybe = (_ -> None) | Some Some(a) | Some(b) => Some(a|b) Maybe(a) | Maybe(b) => Maybe(a|b) * List List(a) = Nil | Cons(a, List(a)) Cons(a, Nil) | Cons(b, Nil) => Cons(a|b, Nil) List(a) | List(b) => is NOT List(a|b) * AA AB(a) = A(a) | B(a) aka AB = A | B A(a) | A(b) => A(a|b) AB(a) | AB(b) => is NOT AB(a|b) So in which case c(a) | c(b) => c(a|b) ?? Well: - if c is recursive (eg: List), it doesn't work (?) => it doesn't work for List - if c(a) = e1 | e2 | ... | en where only one ei use "a", it works => it works for Maybe (only Some use "a") => it doesn't work for AA (both A and B use "a") History: i told Alain Frisch that "c(a) | c(b) => c(a|b)" was true in any case which of course is false (he showed me i was wrong, thanks to him). Terminology: I don't know what's the terminology for this propriety: c(a) | c(b) !< c(a|b) holds if "c" is covariant c(a) | c(b) !> c(a|b) holds if "c" is ??? when "c" is contravariant, we have c(a) |&| c(b) !> c(a|b) and also c(a) | c(b) !> c(a|b) (since c(a) | c(b) !> c(a) !> c(a) |&| c(b)) but Maybe is not contravariant. It is something in the middle... More: if c(a) | c(b) => c(a|b) we also have c(a) |&| c(b) => c(a|&|b) ```
 [merd-devel] Re: typage From: Alain Frisch - 2001-11-24 16:00:16 ```On 24 Nov 2001, Pixel wrote: > je vois vraiment pas comment une intersection peut marcher. A moins de = passer > par la n=E9gation : Oui, pr=E9cisemment. Un paquet c'est un ensemble fini de valeurs, donc un =E9l=E9ment de Pf(D) (parties finies incluses dans D, ensemble des valeurs). Le type {t}, ce sont ceux qui intersectent t, ie qui ne sont pas incluses le complementaire de t, ie qui ne sont pas elements de Pf(\neg t). Donc {t} =3D Pf(D) \ Pf (D \ t) Alain ```
 [merd-devel] Re: typage From: Pixel - 2001-11-24 15:48:56 ```Alain Frisch writes: > On 24 Nov 2001, Pixel wrote: > > > > Ok; vu le nom, j'imagine que si v1 a le type t1 et v2 le type t2, > > > v1 & v2 a le type (t1 inter t2). Argh, mais du coup, ce type ne > > > peut pas être vide, quels que soient t1 et t2. Par exemple, > > > int inter (int -> int) n'est pas vide. Yups, je vois mal comment > > > definir le sous-typage. > > > > c clair que ce n'est plus l'intersection sur les ensembles. C'est plus un > > constructeur. Ca autorise du sous-typage dans le sens inverse de la réunion. > > Et pourtant ... tu as apparemment une regle de sous-typage: > (t1 & t2) <= t1 qui te permet d'utiliser implicitement les valeurs de > type (t1 & t2) dans un contexte où on attend une valeur de type t1. ben oui, c'est l'inverse de la réunion... (t1 & t2) <= t1 <= (t1 \/ t2) > > > J'ai vu qque part un type du genre "int inter (int -> int)" pour > > avoir des paramètres par défaut. > > > > f :: int -> (int /\ (int -> int)) > > > > ça autorise "f 1 + 1" et "f 1 2 + 1" > > Je vois bien comment attaquer ça dans mon formalisme, mais avec une > fonction de coercion explicite (t1 & t2 -> t1). Plus précisemment, > j'introduis un nouvel univers de types, dont les types atomiques > sont notés { t }. Ca s'interprete comme un paquet de valeurs dont > au moins un est de type t. Ainsi: t1 & t2 = {t1} \inter {t2} > (avec \inter une vraie intersection ensembliste), je vois vraiment pas comment une intersection peut marcher. A moins de passer par la négation : superposition de 0 et 1: 0 & 1 = Encode(0) \inter Encode(1) avec Encode(t) = T \ { t } donc 0 & 1 = T \ { 0 } \inter T \ { 1 } = T \ { 0, 1 } donc 0 & 1 < 0 puisque Encode(0 & 1) inclus dans Encode(0) ```
 [merd-devel] Re: typage From: Alain Frisch - 2001-11-24 14:21:59 ```On 24 Nov 2001, Pixel wrote: > > Ok; vu le nom, j'imagine que si v1 a le type t1 et v2 le type t2, > > v1 & v2 a le type (t1 inter t2). Argh, mais du coup, ce type ne > > peut pas =EAtre vide, quels que soient t1 et t2. Par exemple, > > int inter (int -> int) n'est pas vide. Yups, je vois mal comment > > definir le sous-typage. > > c clair que ce n'est plus l'intersection sur les ensembles. C'est plus = un > constructeur. Ca autorise du sous-typage dans le sens inverse de la r=E9= union. Et pourtant ... tu as apparemment une regle de sous-typage: (t1 & t2) <=3D t1 qui te permet d'utiliser implicitement les valeurs de type (t1 & t2) dans un contexte o=F9 on attend une valeur de type t1. > J'ai vu qque part un type du genre "int inter (int -> int)" pour > avoir des param=E8tres par d=E9faut. > > f :: int -> (int /\ (int -> int)) > > =E7a autorise "f 1 + 1" et "f 1 2 + 1" Je vois bien comment attaquer =E7a dans mon formalisme, mais avec une fonction de coercion explicite (t1 & t2 -> t1). Plus pr=E9cisemment, j'introduis un nouvel univers de types, dont les types atomiques sont not=E9s { t }. Ca s'interprete comme un paquet de valeurs dont au moins un est de type t. Ainsi: t1 & t2 =3D {t1} \inter {t2} (avec \inter une vraie intersection ensembliste), et un calcul permet d'obtenir les relations de sous-typages pour cet univers: inter des {t_i} <=3D union des {s_j} ssi il existe i. t_i <=3D union des s_j Apr=E8s, on introduit un operateur "pick_t" pour chaque type t, qui donne en particulier pick_t ({t}) =3D t. On utilise cet operateur pour retrouver explicitement dans un paquet un =E9l=E9ment de type t. Enfin, ca revient en gros =E0 utiliser un type liste (ou plutot arbre binaire) ... A+ Alain ```
 [merd-devel] Re: typage From: Pixel - 2001-11-24 13:20:11 ```Alain Frisch writes: > On 23 Nov 2001, Pixel wrote: > > > v1 & v2 est une *valeur*, donc tu prends v1 & v2 (au niveau de > > l'implémentation, ça risque d'etre coton à optimiser, c'est clair). > > Ok; vu le nom, j'imagine que si v1 a le type t1 et v2 le type t2, > v1 & v2 a le type (t1 inter t2). Argh, mais du coup, ce type ne > peut pas être vide, quels que soient t1 et t2. Par exemple, > int inter (int -> int) n'est pas vide. Yups, je vois mal comment > definir le sous-typage. c clair que ce n'est plus l'intersection sur les ensembles. C'est plus un constructeur. Ca autorise du sous-typage dans le sens inverse de la réunion. J'ai vu qque part un type du genre "int inter (int -> int)" pour avoir des paramètres par défaut. f :: int -> (int /\ (int -> int)) ça autorise "f 1 + 1" et "f 1 2 + 1" ya ça dans http://www.cse.ogi.edu/~mbs/pub/type_indexed_rows/, mais je l'ai déjà vu ailleurs. > (désolé, j'ai pas encore trouvé le temps > de regarder merd) > > > je reformule donc : est-ce que t'as un moyen d'exprimer le fait que c'est le > > record à le meme type sur les champs autre que x. > > Non. J'ai en tête d'etendre le polymorphisme paramétrique pour avoir > des variables de rangées comme en Caml ... j'ai trouvé un papier qui m'a l'air intéressant (au cas ou tu ne connaitrai pas bien sur :) : http://www.informatik.fernuni-hagen.de/import/pi8/papers/res/WideraBeierle2000-SFP99.abstract.html je suis en train de chercher comment implémenter le plus efficacement possible un treillis basé sur une relation d'ordre partielle (le but est de minimiser le nombre de comparaisons). fonctions: - pour un élément donné, quelles sont les éléments du treillis qui sont inférieurs (resp. supérieurs) type: t -> lattice t -> [t] - ajouter un élément au treillis type: t -> lattice t -> lattice t - quelles sont les bornes inférieures (resp. supérieures) (ça c'est facile) type: lattice t -> [t] j'imagine que c'est bien connu, mais je n'arrive pas à trouver sur google. merci, Pixel. ```
 [merd-devel] Re: typage From: Alain Frisch - 2001-11-24 12:29:19 ```On 23 Nov 2001, Pixel wrote: > v1 & v2 est une *valeur*, donc tu prends v1 & v2 (au niveau de > l'impl=E9mentation, =E7a risque d'etre coton =E0 optimiser, c'est clair= ). Ok; vu le nom, j'imagine que si v1 a le type t1 et v2 le type t2, v1 & v2 a le type (t1 inter t2). Argh, mais du coup, ce type ne peut pas =EAtre vide, quels que soient t1 et t2. Par exemple, int inter (int -> int) n'est pas vide. Yups, je vois mal comment definir le sous-typage. (d=E9sol=E9, j'ai pas encore trouv=E9 le temps de regarder merd) > je reformule donc : est-ce que t'as un moyen d'exprimer le fait que c'e= st le > record =E0 le meme type sur les champs autre que x. Non. J'ai en t=EAte d'etendre le polymorphisme param=E9trique pour avoir des variables de rang=E9es comme en Caml ... Alain ```
 [merd-devel] Re: typage From: Pixel - 2001-11-23 21:53:14 ```Alain Frisch writes: > On 23 Nov 2001, Pixel wrote: > > > > C'est quoi, intersection values ? Une valeur obtenue en prenant la > > > conjonction de deux valeurs ? Pour les fonctions, j'imagine que ca > > > ressemble à une fonction surchargée, mais pour les autres valeurs, > > > je ne vois pas. Peut-être une valeur qui s'adapte suivant le contexte > > > où elle est utilisée, en redevenant une des deux valeurs qui la compose ? > > > > oui, tout à fait. > > cf http://merd.net/types.html#intersection > > je ne sais pas si ça vaut le coup pour le "free intersection values". > > Ok. Le problème, c'est quand il y a ambiguité, non ? > Si tu considères (v1 & v2), avec v1 de type t1, v2 de type t2, > et que tu l'utilises dans le contexte (t1 inter t2), tu prends quoi ? > v1 ou v2 ? v1 & v2 est une *valeur*, donc tu prends v1 & v2 (au niveau de l'implémentation, ça risque d'etre coton à optimiser, c'est clair). dans le papier Shields/Meijer, le pb qu'il essaie de résoudre, c'est d'interdire : i : Int j : Int i & j : Int parce que sémantiquement, il n'en veut pas. Perso, je pensais écraser la valeur précédente. Ça rend l'opérateur d'intersection non symétrique quand il y a le meme type des 2 cotés. J'avoue que j'ai pas vraiment réfléchi au pb, je me le réserve pour plus tard, en espérant que quelqu'un aura trouvé une réponse qui me plaise :) > > > [ x:int ; y:int ] -> [ x:int ; z:int ] < [ x : int ] -> [ x : int ] > > > > c'est vrai ? > > Non, [x : int] n'est pas sous-type de [ x:int ; y:int ] > (dans le deuxième type, on a forcément le champ y, pas dans le premier). ...??..? à ça y ait ! je viens de voir que le type du résultat ne parlait pas du champ "y" qu'il y avait en entrée... je reformule donc : est-ce que t'as un moyen d'exprimer le fait que c'est le record à le meme type sur les champs autre que x. c-à-d : my_rec = { x = 2 ; y = "Hello World" } |- [\$ x : 2 ; y : string ] f my_rec |- [\$ x : int ; y : string ] ```
 [merd-devel] Re: typage From: Alain Frisch - 2001-11-23 21:30:51 ```On 23 Nov 2001, Pixel wrote: > > C'est quoi, intersection values ? Une valeur obtenue en prenant la > > conjonction de deux valeurs ? Pour les fonctions, j'imagine que ca > > ressemble =E0 une fonction surcharg=E9e, mais pour les autres valeurs= , > > je ne vois pas. Peut-=EAtre une valeur qui s'adapte suivant le contex= te > > o=F9 elle est utilis=E9e, en redevenant une des deux valeurs qui la c= ompose ? > > oui, tout =E0 fait. > cf http://merd.net/types.html#intersection > je ne sais pas si =E7a vaut le coup pour le "free intersection values". > > par contre, =E7a marche bien (je trouve) pour l'overloading, les record= s, > l'h=E9ritage d'interface. > > le seul papier que je connaisse qui parle de =E7a, c'est > http://www.cse.ogi.edu/~mbs/pub/type_indexed_rows/ Ok. Le probl=E8me, c'est quand il y a ambiguit=E9, non ? Si tu consid=E8res (v1 & v2), avec v1 de type t1, v2 de type t2, et que tu l'utilises dans le contexte (t1 inter t2), tu prends quoi ? v1 ou v2 ? > [ x:int ; y:int ] -> [ x:int ; z:int ] < [ x : int ] -> [ x : int ] > > c'est vrai ? Non, [x : int] n'est pas sous-type de [ x:int ; y:int ] (dans le deuxi=E8me type, on a forc=E9ment le champ y, pas dans le premie= r). Alain ```
 [merd-devel] Re: typage From: Pixel - 2001-11-23 21:20:42 ```Alain Frisch writes: > On 23 Nov 2001, Pixel wrote: > > > Il y a pas mal de points communs entre nos 2 approches du système de types. > > Une différence importante, c'est que le système de types de merd est > > complètement basé sur la sémantique et doit surement etre incorrect/incohérent > > dans les coins (ou pire...). > > Qu'est-ce que tu appelles "basé sur la sémantique" ? C'est aussi > ce que j'essaye de faire, en obtenant par exemple que (t <= s) > signifie exactement que toutes les expressions de type t sont > de type s, ou que (t1.t2) [le type du résultat de l'application > d'une fonction de type t1 a un argument de type t2] est > denote exactement l'ensemble des valeurs que l'on peut obtenir > en appliquant une fonction de type t1 a un argument de type t2. d'accord, mais je pensais plutot aux règles de réécriture/simplification que j'utilise qui ne sont basés sur pas grand chose. > > > - "type vide". Résultat je ne peux pas faire "t?" et plein d'autres trucs. Je > > ne sais pas trop comment ça s'intègre au niveau de l'inférence... > > t? ca veut dire (t option) ? Si oui, tu n'as pas besoin du type vide, > c'est juste un type somme comme en ML. tu veux dire t? = t | () ? en fait, j'ai du mal à voir les utilisations, surtout avec inférence de type. A priori, ça s'utilise sur les tuples pour les transformer en liste. Déjà, j'ai un pb vu que List(Int, String) contient des couples, ya un pb pour applatir. En disant que (Int, String)* c'est un genre de liste avec applatissement. On obtient des trucs du genre : (1, 1, 2, 1, 1) < (1, 1, 2?)* (1, 1, 2, 1, 1) < (1+, 2?)* (1, 1, 2, 1, 1) < (1|2)* mais là encore, le "+" et le "?" applatisse. Il faudrait que 2? = (2) | () avec 2 un tuple d'un élément. J'ai un pb de syntaxe/structure de données sur ce truc là... J'arrive pas à le faire tenir dans un langage classique... [...] > > Trucs qu'il y a dans merd : > > - intersection values. Je n'arrive pas trop à savoir si c'est présent dans ton > > système de types. Le "&" dans le filtrage sert à contraindre/rafiner. Peut-on > > l'utiliser pour construire ? > > C'est quoi, intersection values ? Une valeur obtenue en prenant la > conjonction de deux valeurs ? Pour les fonctions, j'imagine que ca > ressemble à une fonction surchargée, mais pour les autres valeurs, > je ne vois pas. Peut-être une valeur qui s'adapte suivant le contexte > où elle est utilisée, en redevenant une des deux valeurs qui la compose ? oui, tout à fait. cf http://merd.net/types.html#intersection je ne sais pas si ça vaut le coup pour le "free intersection values". par contre, ça marche bien (je trouve) pour l'overloading, les records, l'héritage d'interface. le seul papier que je connaisse qui parle de ça, c'est http://www.cse.ogi.edu/~mbs/pub/type_indexed_rows/ > > > - bounded polymorphisme. Permet entre autre de généraliser le row subtyping : > > [ x : int ] -> [\$ x : int ] qui veut dire t1 -> t2 avec t1 < [\$x:int], t2 = [\$x:int] > > [ x : int ] -> [ x : int ] qui veut dire t1 -> t2 avec t1 < [\$x:int], t2 < [\$x:int] > > devient > > X(Int) -> X(Int) qui veut dire t1 -> t2 avec t1 < X(Int), t2 > X(Int) est equivalent à [ x : int ] -> [\$ x : int ] et [\$ x : int ] -> [\$ x : int ], il interdit la subsomption en entrée ? > > x -> (x !< X(Int)) ; x ici je dis que c'est le meme record (ya les meme champs) en sortie et en entrée (ce qui est classique en OO) > > Je ne comprends pas trop ... > > > du moins si j'ai bien compris, est-ce que > > [\$ x:int ; y:int ] -> [\$ x:int ; z:int ] < [ x : int ] -> [ x : int ] > > ?? > > Dans mon système, non. Il faudrait que [x : int] < [\$ x : int; y : int] > ce qui est faux (le premier type signifie que le champ x est > de type int; le deuxième que les deux champs x et y ont le type int, > mais aussi qu'il n'y a aucun autre champ présent). et [ x:int ; y:int ] -> [ x:int ; z:int ] < [ x : int ] -> [ x : int ] c'est vrai ? ```
 [merd-devel] Re: typage From: Alain Frisch - 2001-11-23 20:46:53 ```On 23 Nov 2001, Pixel wrote: > Il y a pas mal de points communs entre nos 2 approches du syst=E8me de = types. > Une diff=E9rence importante, c'est que le syst=E8me de types de merd es= t > compl=E8tement bas=E9 sur la s=E9mantique et doit surement etre incorre= ct/incoh=E9rent > dans les coins (ou pire...). Qu'est-ce que tu appelles "bas=E9 sur la s=E9mantique" ? C'est aussi ce que j'essaye de faire, en obtenant par exemple que (t <=3D s) signifie exactement que toutes les expressions de type t sont de type s, ou que (t1.t2) [le type du r=E9sultat de l'application d'une fonction de type t1 a un argument de type t2] est denote exactement l'ensemble des valeurs que l'on peut obtenir en appliquant une fonction de type t1 a un argument de type t2. > - "type vide". R=E9sultat je ne peux pas faire "t?" et plein d'autres t= rucs. Je > ne sais pas trop comment =E7a s'int=E8gre au niveau de l'inf=E9rence... t? ca veut dire (t option) ? Si oui, tu n'as pas besoin du type vide, c'est juste un type somme comme en ML. > C'est int=E9ressant, j'aimerais voir l'utilit=E9 dans un programme =ABc= lassique=BB (=E7a > a l'air puissant pour le XML) Par definition, un programme de type vide ne peut pas terminer (car son r=E9sultat serait une valeur de type vide !). > Trucs qu'il y a dans merd : > - intersection values. Je n'arrive pas trop =E0 savoir si c'est pr=E9se= nt dans ton > syst=E8me de types. Le "&" dans le filtrage sert =E0 contraindre/rafine= r. Peut-on > l'utiliser pour construire ? C'est quoi, intersection values ? Une valeur obtenue en prenant la conjonction de deux valeurs ? Pour les fonctions, j'imagine que ca ressemble =E0 une fonction surcharg=E9e, mais pour les autres valeurs, je ne vois pas. Peut-=EAtre une valeur qui s'adapte suivant le contexte o=F9 elle est utilis=E9e, en redevenant une des deux valeurs qui la compo= se ? > - bounded polymorphisme. Permet entre autre de g=E9n=E9raliser le row s= ubtyping : > [ x : int ] -> [\$ x : int ] qui veut dire t1 -> t2 avec t1 < [\$x:i= nt], t2 =3D [\$x:int] > [ x : int ] -> [ x : int ] qui veut dire t1 -> t2 avec t1 < [\$x:i= nt], t2 < [\$x:int] > devient > X(Int) -> X(Int) qui veut dire t1 -> t2 avec t1 < X(Int= ), t2 > X(Int) > x -> (x !< X(Int)) ; x Je ne comprends pas trop ... > du moins si j'ai bien compris, est-ce que > [\$ x:int ; y:int ] -> [\$ x:int ; z:int ] < [ x : int ] -> [ x : in= t ] > ?? Dans mon syst=E8me, non. Il faudrait que [x : int] < [\$ x : int; y : int] ce qui est faux (le premier type signifie que le champ x est de type int; le deuxi=E8me que les deux champs x et y ont le type int, mais aussi qu'il n'y a aucun autre champ pr=E9sent). A+ Alain ```
 [merd-devel] typage From: Pixel - 2001-11-23 20:18:35 ```J'ai fini de regarder ton mémoire[1]. J'ai eu sacrément du mal à comprendre quoique ce soit dans les chapitres 2, 3, 4. L'annexe A m'a bien aidé à comprendre :) Il y a pas mal de points communs entre nos 2 approches du système de types. Une différence importante, c'est que le système de types de merd est complètement basé sur la sémantique et doit surement etre incorrect/incohérent dans les coins (ou pire...). C'est assez intéressant de voir comment le filtrage sur les types peut rejoindre le filtrage sur les valeurs quand les types sont des singletons (ce qui est le cas en merd). Trucs que je n'ai pas dans merd : - "non t" - "type vide". Résultat je ne peux pas faire "t?" et plein d'autres trucs. Je ne sais pas trop comment ça s'intègre au niveau de l'inférence... C'est intéressant, j'aimerais voir l'utilité dans un programme «classique» (ça a l'air puissant pour le XML) - puissant filtrage sur les types. D'un coté, ça se rapproche du RTTI, filter_string ressemble à : def filter_string(l) l.select{|s| s.kind_of?(String)} end filter_string [ 1, 2, "Hello", 3, "World", 4 ] #=> [ "Hello", "World" ] (en ruby, serait similaire en python/perl/...) Trucs que je n'ai pas encore dans merd : - types récursifs: je n'ai pas encore regardé le pb vu qu'en fait je ne m'en sers pas trop en programmation «normale» (aka strings, nombres, tuples, listes (qui sont gérées en dur)...) Trucs qu'il y a dans merd : - intersection values. Je n'arrive pas trop à savoir si c'est présent dans ton système de types. Le "&" dans le filtrage sert à contraindre/rafiner. Peut-on l'utiliser pour construire ? - plus grande simplicité sur les types de base ???? (à part les contraintes de sous-typage) : pas de construction spéciale pour les records (par contre du sucre serait peut-etre nécessaire) - bounded polymorphisme. Permet entre autre de généraliser le row subtyping : [ x : int ] -> [\$ x : int ] qui veut dire t1 -> t2 avec t1 < [\$x:int], t2 = [\$x:int] [ x : int ] -> [ x : int ] qui veut dire t1 -> t2 avec t1 < [\$x:int], t2 < [\$x:int] devient X(Int) -> X(Int) qui veut dire t1 -> t2 avec t1 < X(Int), t2 > X(Int) x -> (x !< X(Int)) ; x du moins si j'ai bien compris, est-ce que [\$ x:int ; y:int ] -> [\$ x:int ; z:int ] < [ x : int ] -> [ x : int ] ?? - inférence de type. Bien sur il n'est pas complet ! Comme dans O'Haskell, des compromis sont faits pour conserver une certaine lisibilité. eg: double(f,x) = f(f(x)) donne (x->x, x) -> x et pas (a->b |&| b->c, a) -> c ou (a->b, a) -> (b !< a) ; b - abstract types et "Open_function" a+ [1] http://www.eleves.ens.fr:8080/home/frisch/dea/rapport.ps.gz ```
 [merd-devel] Re: [very] basic question From: Pixel - 2001-11-21 15:41:33 ```"Robert L. Constable" writes: [...] > Basically, the members of types are structured data elements, and the > type describes the structure, telling how the elements are constructed. this does not go along with many programming languages. In haskell the type of 1 is (Num a => a) which doesn't describe the structure, but what you can *do* with it. Nowadays, types are more and more used to tell what-you-can-do, than what-is-the-structure of a value is. The what-you-can-do philosophy includes the what-is-the-structure (since the what-you-can-do for basic types are given as the minimal functions). what-you-can-do doesn't have any implicit subtyping rules, whereas what-is-the-structure do have implicit subtyping rules. But again many languages do not use implicit subtyping (strutural equivalence), prefering explicit/declared subtyping (declaration equivalence) The result is that there is no more any simple mapping from values to types. Values are tagged into types. If you dissociate values from types, you can still see types as sets, but only for supertyping: solution1: true = True false = False bool supertype of true and false => bool = True \/ False and define the order relation as (classical subsetting) True < True \/ False solution2: vehicle = Vehicle car subtype of vehicle => car = Vehicle /\ Car_ and define the order relation as (inverse of subsetting) Vehicle > Vehicle /\ Car_ - solution1 nicely models extensible variants - solution2 nicely models the OO subtyping - so most languages do not follow any subsetting relation since most languages allow subtyping, but not supertyping. - true, false, bool are variables - True, False, Vehicle, Car_ are simple type constants - the subtyping relation is strictly structural - every normalised types is a union of intersection of basic types - basic types are all unrelied: we have neither C1 subtype of C2 or C2 subtype of C1 - the subtyping relation is defined only on /\ and \/ - normalisation of types is simple (see normalisation of functions below) - Car_ alone is not a legal type, but it won't appear alone in type expressions - programming languages usually do not allow mixing types, in that case an expression can't have type "True /\ Vehicle" or "True \/ Vehicle" [...] > A key practical difference is that functions in the type A->B are > polymorphic whereas those in the set of functions from A to B are not. > This makes subtypes behave differently than subsets, so for example if > A[A' (A is a proper subtype of A') and B[B', then (A'->B)[(A->B'), > i.e. subtyping is co-variant on the domain. This basic difference > shows up in the definition of records for example. the contravariance on parameters and covariance on result is a property of "->" : true -> false defined as True -> False bool -> false defined as True -> False /\ False -> False true -> bool defined as True -> True \/ True -> False bool -> bool defined as (True -> True /\ False -> True) \/ (True -> False /\ False -> False) and we do have bool -> true < true -> true < true -> bool vehicle -> vehicle defined as Vehicle -> Vehicle vehicle -> car defined as Vehicle -> Vehicle /\ Vehicle -> Car_ car -> vehicle defined as Vehicle -> Vehicle \/ Car_ -> Vehicle car -> car defined as (Vehicle -> Vehicle /\ Vehicle -> Car_) \/ (Car_ -> Vehicle /\ Car_ -> Car_) and we do have vehicle -> car < vehicle -> vehicle < car -> vehicle * ad'hoc overloaded functions can be typed: a function over Int returning Int, and also over String returning String (Int -> Int) /\ (String -> String) this type is compatible with: (Int -> Int) /\ (String -> String) < (Int -> Int) (Int -> Int) /\ (String -> String) < (String -> String) (some more at http://merd.net/pixel/language-study/types.txt) -- Pixel programming languages addict http://merd.net/pixel/language-study/ ```
 [merd-devel] [Didier Remy ] Re: [Caml-list] [Q]: Co(ntra)variance and subtyping? From: Pixel - 2001-11-20 20:50:34 ```more on type inference completeness -------------------- Start of forwarded message -------------------- X-From-Line: pixel Tue Nov 20 10:58:23 2001 Return-Path: Received: from 216.71.116.162 [216.71.116.162] by localhost with IMAP (fetchmail-5.9.5) for pixel@... (single-drop); Tue, 20 Nov 2001 10:58:23 +0100 (CET) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by mandrakesoft.mandrakesoft.com (8.8.5/8.8.5) with ESMTP id DAA15316 for ; Tue, 20 Nov 2001 03:58:12 -0600 Received: from morgon.inria.fr (morgon.inria.fr [128.93.8.33]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id fAK9w8b25481; Tue, 20 Nov 2001 10:58:08 +0100 (MET) Received: (from remy@...) by morgon.inria.fr (8.11.6/8.11.6) id fAK9w0C08700; Tue, 20 Nov 2001 10:58:00 +0100 To: Alain Frisch Cc: Jacques Garrigue , , Subject: Re: [Caml-list] [Q]: Co(ntra)variance and subtyping? References: From: Didier Remy Date: 20 Nov 2001 10:58:00 +0100 In-Reply-To: Message-ID: User-Agent: Gnus/5.0808 (Gnus v5.8.8) Emacs/20.7 X-MIME-Autoconverted: from quoted-printable to 8bit by mandrakesoft.mandrakesoft.com id DAA15316 Xref: leia.mandrakesoft.com mail.caml:4424 Lines: 62 Alain Frisch writes: > > In the ML world, we mean complete type inference. > > What does complete type inference mean ? I would say that it implies > that no type annotation is mandatory (if a program typechecks with a type > annotation, it should also typecheck without). This property does not hold > in OCaml; you can't remove type annotation in: > > class o = object method f (x : int) = x end Just to mention that examples can also be found in (almost) the core language as well, you could choose ``ref []'' alone, which program will be rejected by the compiler. ---------------- I take this opportunity to raise a question about the meaning of "type inference". Indeed, the answer of whether a language has type inference may be more subtle than it first appears. Checking whether types are/must be mentioned in source programs may not be sufficient. Consider data-type declarations: type 'a list = [] | Cons of 'a * 'a list Is this a type annotation? Indeed, this declaration amounts to later implicitly annotate every occurrence of a Cons as carrying arguments of types 'a and 'a list. The situation apparently looks simpler for the raw lambda-calculus, which comes in two flavors untyped and typed and where the untyped version does not mention types at all. However, there is no untyped version of ML (with datatypes/exceptions, etc.) in the sense that types would not be mentioned at all. Even in the lambda-calculus it should be fair to consider that (fun x -> a) carries the (implicit) type annotations ('a -> 'b). So, isn't it unfair to make a difference between type annotations that are plugged into the syntax and more elaborated type annotations that would are explicitly in the syntax. Formally, the distinction is not obvious: syntactic nodes (_ : t) can well be seen as (i.e. replaced by) built-in primitives of types t -> t (and given the same semantics as the identity). Hopefully, there is always a lot of type information in programs, whether it is implicit or explicit ---otherwise, type inference could not do much. Furthermore, the difference between explicit and implicit annotations is not always so clear, certainly not a binary notion. My conclusions are that - the typed and untyped version cannot be left implicit when talking about type inference. - the property of ``having type inference'' should rather be replaced by a measure of ``how much type inference'' (1) or ``what are the properties of type inference'' (2). Answers to (2) the later can be made formal. Answers to (1) tend to be informal ---but it would be interesting to find a formal criteria... Didier Rémy -------------------- End of forwarded message -------------------- ```
 [merd-devel] Re: demande de commentaires et pointeurs From: Pixel - 2001-11-16 16:17:54 ```Francois Pottier writes: > Salut, > > > Si haskell n'est pas complet, ça ne me pose pas de pb que merd ne le soit pas > > Haskell est complet pour autant que je sache... essaye [] == [] et ensuite [] == ([] :: [Int]) [...] > > Ce que veut le programmeur c'est que ça fasse ce qu'il veut. > > Oui... c'est là que la notion de complétude de l'inférence joue un rôle > malgré tout assez important. Un système de types, c'est > > + un langage permettant d'exprimer des preuves de correction de programmes > (le langage des dérivations de typage); et > > + un algorithme permettant de construire automatiquement de telles preuves > (l'algorithme d'inférence). > > On peut voir le premier comme une spécification du second. La propriété de > complétude consiste à dire que, s'il existe une façon de prouver que le > programme est correct, alors l'algorithme la découvrira. > > L'idée, c'est que le langage de preuves (le système de types) est souvent plus > simple que l'algorithme de reconstruction. Si ce dernier est complet, on peut > expliquer le premier seulement à l'utilisateur, et tout ira bien. En l'absence > de complétude, l'utilisateur doit comprendre non seulement le système de > types, mais aussi le fonctionnement de l'algorithme, pour savoir quand et > comment annoter son programme. Je ne connais pas de langages à base d'inférence de types qui permettent au programmeur de se passer de comprendre l'algorithme d'inférence. Par exemple en ML, quand il y a des fonctions récursives, c'est dur d'expliquer : # let rec ff x = gg (x + 1) and gg x = x ^ "foo";; ^ This expression has type int but is here used with type string à cause du fait que l'algo est gauche->droite, ce qui n'est pas forcément le message auquel le programmeur s'attend. Comment expliquer au programmeur que pour avoir l'information que c'est l'appel du dessus qui est faux, qu'il faille rajouter # let rec ff x = gg (x + 1) ^^^^^^^ and (gg : string -> string) = fun x -> x ^ "foo";; This expression has type int but is here used with type string Bien sur il y a des degrés entre les différents algo. Il est plus dur de comprendre l'inférence de haskell que celle de caml (en utilisant pas de polymorphic variants) > > Cela dit, c'est vrai qu'on peut toujours tordre la spécification pour la faire > coller à un algorithme mal conçu, donc il reste une dose d'arbitraire dans > cette idée. Disons que `idéalement' la spécification du système est simple et > élégante et l'algorithme (potentiellement complexe) est complet, ce qui évite > de se demander comment il marche. je suis d'accord sur le fait que la complétude, c'est mieux. je ne suis pas d'accord sur le fait que la complétude permet de se passer de comprendre l'inférence. > > J'espère que ça éclaircit un peu notre position. > > > - l'intersection en générale, c'est ??? > > Oui c'est un peu ce que je me disais :) > > D'après ce que je comprends de tes exemples, tu pourrais être intéressé par > l'article `Type-Indexed Rows' (Mark Shields et Erik Meijer). Peut-être aussi > par le `polytypic programming' (http://www.cs.chalmers.se/~patrikj/poly/). ok, je vais regarder, merci. Pixel. ```
 [merd-devel] Re: demande de commentaires et pointeurs From: Pixel - 2001-11-16 14:25:15 ```Francois Pottier writes: [...] > > j'essaye maintenant de me renseigner le plus possible pour savoir si des > > expérimentations de ce genre de système de type existent. Mais la plupart des > > papiers que je trouvent sont illisibles de mon point de vue : j'y cherche des > > maigres exemples pour me faire une idée, mais j'ai vraiment du mal :-/ > > Oui, c'est-à-dire que les chercheurs commencent toujours par s'intéresser aux > propriétés théoriques du langage, même s'ils ont une véritable implantation en > vue. On peut le critiquer, mais je trouve tout de même qu'on comprend mieux un > langage en décrivant formellement sa sémantique et son système de types, qu'en > donnant seulement une série d'exemples... un jour je comprendrai peut-etre ça... :) [...] > Quelques mots à propos des problèmes d'inférence que tu décris en bas de ta > page ;. En général, on essaie de définir un > algorithme d'inférence complet (i.e. qui accepte le programme du moment qu'il > est typable). Si haskell n'est pas complet, ça ne me pose pas de pb que merd ne le soit pas ;) En général, je trouve que c'est jouer sur les mots de dire qu'il est complet ou pas. Un système de types restrictif peut-etre complet, mais beaucoup plus contraignant à utiliser qu'un autre plus permissif mais non complet. Ce que veut le programmeur c'est que ça fasse ce qu'il veut. Alors qu'il faille - eta-expand pour passer la monomorphic restriction - ajouter des coercions en ocaml quand on veut faire une liste de points avec des colored_point et des point parce qu'il n'y pas de subtyping, - ajouter des float_of_int au lieu de caster en float, ou ajouter des annotations, je ne vois pas trop la différence. [...] > Effectuer des choix par défaut me semble mauvais (l'utilisateur > n'est pas forcément capable de déterminer où de tels choix ont été faits, et > comment les corriger s'ils ne conviennent pas). Je suis d'accord. Mais il y a des moments où on a pas le choix si on veut conserver une certaine expressivité... Si on pousse le bouchon, on peut dire que caml fait un choix par défaut obligatoire en disant que [] est une liste. Si un langage peut utiliser [] comme un ensemble, mais defaulter sur le type liste, ça ne me parait pas abérrant. Un mode warning peut permettre de détecter ces choix (d'accord, c'est pas la panacée) [...] > La solution `acceptée' (dans > le monde de l'inférence à base de contraintes, en tout cas) lorsqu'on manque > d'informations sur un type (par exemple lorsqu'on a une variable o sous la > main et qu'on voudrait savoir si elle vaut Foo ou Boo) est d'émettre une > contrainte et de la garder jusqu'à ce qu'on sache la résoudre (par exemple une > contrainte de la forme `si o vaut Foo, alors o' vaut Bar, sinon o' vaut > Far'). Le problème, évidemment, c'est que ces contraintes sont lourdes et > apparaissent dans les types inférés, d'où un système vite compliqué, difficile > à implanter et à comprendre. Alors soit on bat en retraite et on laisse tomber > (par exemple, en ML, on n'a pas de surcharge du tout), soit on cherche une > approche qui permette de s'en tirer avec des contraintes plus simples (par > exemple, en Haskell, les contraintes sont de la forme (C alpha) pour dire que > alpha appartient à la classe C, ce qui est raisonnablement léger). tout à fait d'accord. Je pense que les contraintes conditionnelles sont intéressantes pour avoir une meilleure précision, mais ne doivent jamais etre affiché dans un message d'erreurs de type. [...] > Voilà, j'espère que ça peut t'aider. Au fait, je ne comprends pas du tout ce > que fait l'opération 0 |&| 1 dans ton langage (je comprends bien > l'intersection de types, mais pas l'intersection de valeurs). C'est quoi le > résultat de ce calcul? En gros, l'idée c'est d'étendre ce qui se fait sur les records et les fonctions: - l'intersection de fonctions c'est l'overloading - l'intersection de tagged values, c'est les records - l'intersection en générale, c'est ??? 0 |&| 1 n'est pas un très bon exemple 0 |&| False est plus intéressant. C'est une valeur, pas un calcul. (from http://merd.sf.net/types.html#intersection) 0 |&| True is a valid value which can be used both as 0 and True. It needs investigating the advantage of this. Here are some examples: * 1|&|"foo" + 1|&|"bar" gives 2|&|"foobar" * [ 1, "foo" ].map(x -> x + 1|&|"bar") gives [ 2, "foobar" ] * 0 |&| "" |&| [] as a default value to initialize variables * (min, sec) = s.m("(\d+):(\d+)") is a regexp returning type Int|&|String, Int|&|String. This enables: * min * 60 + sec where min and sec are used as numbers * print_string(min) merci pour les liens, Pixel. PS: http://www.tuxfamily.net a des pbs, résultat http://merd.net marche pas en ce moment, http://merd.sf.net marche bien > > > PPPS: j'ai linkchecker (http://linkchecker.sf.net/) dans la mandrake ya pas > > longtemps (j'ai cherché pas mal sur internet, mais je ne suis pas tombé sur > > Big Brother). Comparé à Big Brother, ça donne quoi ? > > Aucune idée, je n'ai pas essayé linkchecker... À vue de nez Big Brother en > fait moins (il ne sort pas d'output dans des formats tordus et ne supporte que > les protocoles http: et file:). Cela dit, si linkchecker est écrit en C, Big linkchecker est en python > Brother est peut-être plus stable sur de très gros jobs; faut voir. ```
 [merd-devel] http://merd.net From: Pixel - 2001-11-15 13:43:34 ```merd is now accessible via http://merd.net (and http://www.merd.net) The official link is now http://merd.net, which is not dependent on sourceforge anymore. It is currently hosted by http://www.tuxfamily.org (which provides free DNS hosting, web hosting, mail hosting) ```
 Re: [merd-devel] printf type inference From: Pixel - 2001-11-14 00:57:01 ```Pixel writes: > tf(s) = > T = string2types((), s) > T -> String this was a little optimistic... Here is something that works: n2types = 0 -> () n -> Builtin::tuple_add(Int, n2types(n-1)) tf(n) = T = n2types(n) Builtin::Freeze(Builtin::Expand(T) -> Builtin::Expand(String)) f !! x -> tf(x) z0 = f(0) z1 = f(1) z2 = f(2) gives z0 !! () -> Int z1 !! Int -> Int z2 !! Int,Int -> Int - note the Builtin::Freeze and Builtin::Expand, ugly but easy for me :) - Builtin::Freeze is alike lisp's quote which enables expression to be verbatim. - in fact, i wanted to use Builtin::Freeze for something else... but i should get rid of it one day... ```
 Re: [merd-devel] division and type classes From: Yoann Padioleau - 2001-11-13 13:37:13 ```Pixel writes: > Haskell defines "/" as Fractional a => a -> a -> a > > Which means > div4 l = length l / 4 > is illegal since length returns an Int and Int is not Fractional. i have tried: length2:: Num a => [b] -> a length2 [] = 0 length2 (x:xs) = 1 + length2 xs div4 :: Fractional a => [b] -> a div4 l = length2 l / 4 and it works. > > the pb comes from Int having no subtyping relationship with > Integer/Double/Fraction/Rational the pb comes from the fact that they decide to put length:: [a] -> Int to have less pb of ambiguity lated. > > in merd: > > div4(l) = l.size / 4 > # (l.size returns an UInt) > #=> (4 !< x ; UInt !< x ; x !< &Fractional ; x) > #=> (UInt !< x !< &Fractional ; x) (since 4 !< UInt) > > closing world of (UInt !< x !< &Fractional ; x) gives > - &Fractional instanced by Big_rat (full bignum/bignum) and Double > - both Big_rat and Double are superset of UInt > - so there are 2 solutions Big_rat and Double > - choosing between the 2 must be done somehow... (using a default seems a > solution) > > > PS: were it be x/-4 the constraint would have been > (4 !< x ; UInt !< x ; x !< &Fractional ; x) > with no simplification, but the result would have been the same. > > > _______________________________________________ > Merd-devel mailing list > Merd-devel@... > https://lists.sourceforge.net/lists/listinfo/merd-devel > -- Yoann Padioleau, INSA de Rennes, France, Opinions expressed here are only mine. Je n'écris qu'à titre personnel. **____ Get Free. Be Smart. Simply use Linux and Free Software. ____** ```
 [merd-devel] division and type classes From: Pixel - 2001-11-13 13:26:45 ```Haskell defines "/" as Fractional a => a -> a -> a Which means div4 l = length l / 4 is illegal since length returns an Int and Int is not Fractional. the pb comes from Int having no subtyping relationship with Integer/Double/Fraction/Rational in merd: div4(l) = l.size / 4 # (l.size returns an UInt) #=> (4 !< x ; UInt !< x ; x !< &Fractional ; x) #=> (UInt !< x !< &Fractional ; x) (since 4 !< UInt) closing world of (UInt !< x !< &Fractional ; x) gives - &Fractional instanced by Big_rat (full bignum/bignum) and Double - both Big_rat and Double are superset of UInt - so there are 2 solutions Big_rat and Double - choosing between the 2 must be done somehow... (using a default seems a solution) PS: were it be x/-4 the constraint would have been (4 !< x ; UInt !< x ; x !< &Fractional ; x) with no simplification, but the result would have been the same. ```
 Re: [merd-devel] another argument for the curry notation vs tuple notation From: Pixel - 2001-11-12 13:54:01 ```Yoann Padioleau writes: > you mean > f1(x) = (print "f2 called" ; y -> x+y) > and not f1(x,y) = ... oops, thanks. ```
 Re: [merd-devel] another argument for the curry notation vs tuple notation From: Yoann Padioleau - 2001-11-12 13:49:57 ```Pixel writes: > ! ML partial application mix up two different beasts: > * let f1 x y = x + y which needs both arguments to compute something > * let f2 x = (print "f2 called" ; fun y -> x + y) which really > produces a function using the first argument. > The time of evalution is different, but the type signatures of f1 > and f2 are the same. This forbids eta-expansion: f2 x is not > equivalent to y -> f2 x y > > merd: > > * no evaluation time problem caused by partial evaluation: > * f1(x,y) = x+y has type Int,Int -> Int and is partial > evaluated using f1(10,) whereas > * f1(x,y) = (print "f2 called" ; y -> x+y) has type Int -> Int > -> Int and is partial evaluated using f1(10) you mean f1(x) = (print "f2 called" ; y -> x+y) and not f1(x,y) = ... > > from http://merd.sf.net/choices_syntax.html#function_calls > > _______________________________________________ > Merd-devel mailing list > Merd-devel@... > https://lists.sourceforge.net/lists/listinfo/merd-devel > -- Yoann Padioleau, INSA de Rennes, France, Opinions expressed here are only mine. Je n'écris qu'à titre personnel. **____ Get Free. Be Smart. Simply use Linux and Free Software. ____** ```
 [merd-devel] printf type inference From: Pixel - 2001-11-12 00:28:30 ```Some good news, goal seems reachable now: tf = "a" -> A->A "b" -> C,C->C f !! x, Builtin::Remaining(y) -> tf(x)(y) f("a",), f("b",,) infered nicely A->A, C,C->C and f("a") f("a",,) f("b",) f("b",,,) rejected saying "missing parameters" or "too many parameters" of course, printf is still harder than this, necessary to compute tuples. But something alike the following should work someday: char2type = "d" -> Int "s" -> String string2types(accu, ) = "" -> accu "%" : c : r -> tuple_add(accu, char2type(c)).string2types(r) _ : r -> accu.string2types(r) tf(s) = T = string2types((), s) T -> String notice - the "%" being both a Char and a String - the local variable T used in the type - () as the empty tuple (??) ```
 Re: [merd-devel] partial evaluation for more precise types From: Pixel - 2001-11-11 18:51:12 ```Pixel writes: > Simpler than cayenne: you don't have to write the function giving the type if > the type can be infered: [...] > f2 = > "d" -> a_number() > "s" -> a_number().raw_to_string > > use_f2(x) = "d".f2, "s".f2, x.f2 > #=> "d"|"s" -> Int, String, Int|String Alas, things are not so simple for bigger examples. The solution i took is separating the type from the code of the function. But alas, it also introduces a big hole in the type system. One day, merd will have a nice intelligent partial evaluator and will get rid of this ugly stuff :-( In the mean-time, things will look like: f2 !! Trusted( "d" -> Int "s" -> String ) f2 = "d" -> a_number() "s" -> a_number().raw_to_string note the infamous Trusted which tells merd not to check if the type of the implementation of f2 corresponds to the given type. It means you can write foolish !! Trusted(String -> Int) foolish(x) = x and merd will still be happy... Hopefully, "Trusted" is to remain little used in normal progs (just like "obj" caml magic) ```
 [merd-devel] another argument for the curry notation vs tuple notation From: Pixel - 2001-11-11 14:29:08 ```! ML partial application mix up two different beasts: * let f1 x y = x + y which needs both arguments to compute something * let f2 x = (print "f2 called" ; fun y -> x + y) which really produces a function using the first argument. The time of evalution is different, but the type signatures of f1 and f2 are the same. This forbids eta-expansion: f2 x is not equivalent to y -> f2 x y merd: * no evaluation time problem caused by partial evaluation: * f1(x,y) = x+y has type Int,Int -> Int and is partial evaluated using f1(10,) whereas * f1(x,y) = (print "f2 called" ; y -> x+y) has type Int -> Int -> Int and is partial evaluated using f1(10) from http://merd.sf.net/choices_syntax.html#function_calls ```

Showing results of 27

1 2 > >> (Page 1 of 2)