User:Corentin.moiny/sandbox/Eff

Eff

Eff est un langage de programmation qui se base sur une approche algébrique. Ce dernier est basé sur des fondements théoriques qui se basent sur les mathématiques. Le langage voit le jour à Ljubljana en Slovénie grâce à Andrej Bauer, Matija Pretnar et Timotej Lazar. Ce projet fait l’objet d’une thèse à Université de Ljubljana en 2012. Il sera ensuite poussé sur GitHub en mars 2015 en code source ouvert et continue d’évoluer depuis. Eff est distribué sous une licence BSD.

Raison d'être

L’idée principale derrière le langage c’est que les effets de calculs sont accessibles via un ensemble d’opérations. Eff est conceptualisé de sorte qu’il puisse réagir aux appels de ses opérations à l’aide de gestionnaire, aussi appelé handlers, pour qu’ensuite le programme ait la capacité de déclencher certaines actions suite aux lancements de ces opérations. C’est grâce à cette nouvelle approche que les programmeurs peuvent explorer de nouvelle technique de programmation. Eff supporte des techniques de programmation qui utilise différentes formes de continuation délimitée comme: le retour sur trace, les algorithmes de parcours en largeur, la sélection fonctionnelle et la coopération multifonctionnelle. Ce dernier est un langage de type statique avec un polymorphisme paramétrique et utilise l’inférence de type.

Histoire

La première version du projet est publiée en 2010. Il est en premier lieu théorisé et ensuite conceptualisé. Il fût introduit lors d'un séminaire à Paris durant la même année. Juqu'en 2012, Eff avait une syntaxe qui se rapprochait de Python pour ensuite être adaptée pour que le langage soit ressenti comme OCaml par ses utilisateurs avec la sortie de Eff 3.0. Le projet est à code source ouvert depuis 2015.

Syntaxe

La syntaxe suit de près celle de OCaml, la notion unique au niveau syntaxique de Eff est la notion d'effet. Il faut noter que le double point-virgule marque la fin d'une instruction. Soit.

let z = "horse";;

Types

Mis à part les types standards, Eff introduit le concept du type effet et du type module (handler). Le type vide (empty) est utilisé pour la description des exceptions. La notion du type effet est un ensemble de symboles utiliser pour les flux d'informations d'écriture ou de lecture. Ce type a pour but de permettre la manipulation des effets algébrique dans Eff qui est la raison d'être du langage.

Effet

Chaque effet vient d'un ensemble d'opérations simples. Ils sont divisés en deux parties: une instance et un symbole d'opération. Exemple avec l'opération decide.

type exemple = effect
    operation decide : unit -> bool
end

Gestionnaire

Les gestionnaires permettent la prise en charge des effets. Cela devient utile lorsque le programmeur a pour but de lancer une certaine action lorsque d'une ou plusieurs autres sont lancés. Ils sont utilisés sous le nom de handler. Par exemple.

handle
  std#print "A";
  std#print "B";
  std#print "C";
  std#print "D" 
with | std#print msg k -> std#print ("I see you tried to print " ^ msg ^ ". Not so fast!\n");;

Exception

Une exception est en réalité un effet avec une seule opération et un résultat vide. Le mot-clé raise désigne cette opération. Par exemple.

type 'a exception = effect
   operation raise : 'a -> empty
end

Expression et calcul

Eff différencie de façon significative les expressions et le calcul à la façon d'une technique de fine-grain appel par valeur notamment développé par Paul Blain Levy, professeur à l'Université de Birmingham. La syntaxe du langage cache ses distinctions et permet aux programmeurs de les mettre ensemble librement.

Particularité du langage

Eff est basé sur une approche algébrique des effets dans lequel les effets de calculs sont modélisés en tant qu’opérations algébriques qui suivent une théorie adaptée au contexte. Les effets communs comme: l'entrée, la sortie, l'état et les exceptions sont des concepts supportés par Eff.

Effet algébrique

L’effet algébrique est une approche informatique basée sur le fait que des comportements impurs sont lancés par des opérations comme les accesseurs, les mutateurs, les écritures, les lectures et les exceptions. L’effet algébrique est le simple fait de prendre en charge ces opérations et d’identifier à l’aide de gestionnaires, que le langage utilise sous le nom de handler, les traitements comme la redirection d’écriture et lectures de fichier, le retour sur trace, le multithreading coopératif et la continuation délimitée. Ce phénomène est la principale particularité du langage. Les gestionnaires sont basés sur un modèle homomorphique induit par le concept d’algèbre libre. Les interactions entre les effets et les gestionnaires donnent naissance à de nouvelles façons de programmer ce qui continue en soi la raison d'être du langage.

Fine grain appel par valeur

Un environnement de programmation appel par valeur est un environnement ou les paramètres sont évalués avant la fonction elle-même. Fine grain appel par valeur est similaire, mais le système formel du lambda-calcul (ou λ-calcul) y est introduit de sorte que c’est deux éléments donne un modèle de classes complet. La conception de ce modèle de classes se serait basée sur les travaux de Peter J. Freyd concernant la théorie des catégories dans le domaine des structures mathématiques.

Séquençage

Traitement dans lequel on évalue une expression avant de la procéder pour un traitement quelconque. Soit.

 x <- c1 

Une fois c1 évalué, ce dernier pourra être lié a x.

Appel d'opération

L'appel d'une opération passe en premier lieu par l'évaluation du paramètre concernée qui n'est en réalité que l'adresse mémoire à lire. Ensuite, l'effet d'opération peut être procédé. La valeur de retour est assignée à un élément ce qui permet ensuite la continuation.

Types d'effets

Les instances sont les valeurs les plus importantes dans Eff. Ces instances sont fournies d'un type d'effet. Une instance de type exception sera fournie avec un type d'effet. Soit la forme.

 α exception 

Où α représente de l'information supplémentaire qui qualifie l'effet. Chaque type d'effets est déclaré avec une signature qui liste toutes les opérations disponibles avec le type d'effet concerné.

Type de contrôle

Les types dans Eff sont similaires au standard ML de programmation dans le sens où ils ne capturent aucune information par rapport aux effets de calculs. Eff est un langage qui fonctionne avec l'inférence de type, donc le programmeur ne prend pas en considération le type de ses expressions lors de la déclaration. Par exemple.

input:  let x = 90;;
result: val x : int = 90

input:  let y = "dog";;
result: val y : string = "dog"

Exemples de code

Choix

Opération à choix binaire qui prend une valeur booléenne qui est décrite par un type effet à une seule opération decide.

type choice = effect
  operation decide : unit -> bool
end

let c = new choice

let x = (if c#decide () then 10 else 20) in
let y = (if c#decide () then 0 else 5) in
  x - y

Les expressions x et y se verront assigné une valeur booléenne suivant la sortie de l'opération decide de c. L'opération doit être prise en charge par un gestionnaire pour avoir un résultat.

handle
  let x = (if c#decide () then 10 else 20) in
  let y = (if c#decide () then 0 else 5) in 
    x - y
with
| c#decide () k -> k true

result: x = 10, y = 0

Transaction

Dans le cas où l'on voudrait conserver l'état d'une expression si une exception est levée.

let transaction r = handler
| r#lookup () k -> (fun s -> s s)
| r#update s' k -> (fun s -> () s')
| val x -> (fun s -> r := s; x)
| finally f -> f !r
with transaction r handle
  r := 23;
  raise e (3 * !r);
  r := 34