Si je reprend le code d'exemple :
ça c'est bien un gadt ?
type 'a exp_dic =
{lit : int -> 'a;
neg : 'a -> 'a;
add : 'a * 'a -> 'a};;
ça c'est la définition de la sémantique de "Lit" qui retourne une fonction de construction d'un type ?
let lit : int -> exp = fun x ->
{expi = fun d -> d.lit x}
Que signifie la syntaxe : {expi = ...} ? C'est la création d'un type avec un champs expi ?
ça c'est l'éval :
let eval1 : exp -> int = fun {expi = e} ->
e {lit = (fun x -> x);
neg = (fun e -> - e);
add = (fun (e1,e2) -> e1 + e2)};;
Que signifie la syntaxe "fun {expi = e}" ? et qu'est-ce que le terme "e {...}" ?
[^] # Re: Dans l'art voluptueuse de ne rien comprendre
Posté par Nicolas Boulay (site web personnel) . En réponse au journal EDSL et F-algèbres. Évalué à 2.
Si je reprend le code d'exemple :
ça c'est bien un gadt ?
type 'a exp_dic =
{lit : int -> 'a;
neg : 'a -> 'a;
add : 'a * 'a -> 'a};;
ça c'est la définition de la sémantique de "Lit" qui retourne une fonction de construction d'un type ?
let lit : int -> exp = fun x ->
{expi = fun d -> d.lit x}
Que signifie la syntaxe : {expi = ...} ? C'est la création d'un type avec un champs expi ?
ça c'est l'éval :
let eval1 : exp -> int = fun {expi = e} ->
e {lit = (fun x -> x);
neg = (fun e -> - e);
add = (fun (e1,e2) -> e1 + e2)};;
Que signifie la syntaxe "fun {expi = e}" ? et qu'est-ce que le terme "e {...}" ?
"La première sécurité est la liberté"