Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les références et annexes
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Ven 21 Oct 2011 10:08
Message Les références et annexes
Pour suggérer un ajout ou signaler une erreur, vous pouvez envoyer un message privé.

Avant‑Propos


SML est le nom abrégé de Standard ML, ML étant lui‑même l’acronyme de “Modeling Language”, un langage utilisé dans les expériences avec les programmes de preuves formelles (pour faire des preuves ou assister l’élaboration de preuves), comme les preuves de bon fonctionnement, les preuves de correspondances à des spécifications. Il a donc été surtout utilisé comme une sorte de méta-langage, mais autant ML que SML, sont pourtant aussi des langages généralistes, et ne sont pas réservés à ces domaines particuliers.

Une particularité importante de SML, et qu’il est formellement spécifié, ce qui le distingue des autres plutôt définis de manière pragmatique et empirique. Sa cohérence interne a été démontré.

Ont peut imaginer que SML et ses dérivés ait la faveur des « matheux », dut à ses formulation inspirés des mathématiques (lambda-calcul, curryfication, composition de fonction, expressions pures et sans effets de bords [ou presque, SML n’étant pas tout à fait pure], etc)

Les définitions formelles


La définition de 1997, fait suite à une définition de 1990. La version de 1997 est réputé plus lisible que la version de 1990. La version de 1997 n’est pas accessible en ligne (excepté partiellement) et n’est disponible qu’en livre, pour le prix de 15€ environ :

The Definition of Standard ML, revised edition (mitpress.mit.edu).

Elle est partiellement consultable sur Google Books :

The Definition of Standard ML, revised edition (books.google.fr).

La version précédente, mais obsolète, est disponible en PDF :

The Definition of Standard ML (PDF). 1990. Robin Milner, Mads Tofte, Robert Harper.

Les annexes


La syntaxe concrète de SML comporte quelques points délicats, et des erreurs sont initialement passé inaperçues dans la publication de 1990. Les documents annexes suivants abordent ces aspects.

Commentary on Standard ML (PDF). 1991. Robin Milner, University of Edinburgh; Mads Tofte, University of Nigeria.

Defects in the Revised Definition of Standard ML (PDF). 2007. Andreas Rossberg, Universität des Saarlandes.

Ces documents peuvent aussi être récupéré à cette adresse, au cas où l’un des liens ci-dessus deviendrait invalide :
The Definition of Standard ML (1990) and Commentary on Standard ML (1991).

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Mer 29 Jan 2014 07:10
Message Re: Les références et annexes

Règles de style


Elles sont variables, comme pour la plupart des langages. L’ensemble de règles le plus courant, semble être celui de l’université de Cornell, dans le premier lien. Les deux suivants en dérivent — explicitement pour le second lien, implicitement pour le troisième. Dans le quatrième lien, l’ensemble de règles diffère, par exemple avec la convention de nommage des valeurs, qui n’est plus la convention camel‑case, bien que les règles soient assez proches de celles données dans les trois liens le précédent.


Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Jeu 6 Fév 2014 15:24
Message Re: Les références et annexes

Documentations informelles et quasi‑standards


Ils n’apparaissent pas dans la définition de SML '97, mais ils sont un quasi‑standard d’assez bonne notoriété, supportés par au moins deux compilateurs SML indépendants (ML‑kit et MLton), ce sont les fichiers MLB, pour ML Basis File.

La définition de SML stipule que la « fonction » “use” est “implementation defined”. SML a quelques faiblesses comparé à Ada, en matière de modularité (mais des points forts aussi, qui manquent à Ada, comme les signatures des structures, sans équivalents en Ada), au moins à cause de ce “use” sur lequel on ne peut pas compter (pas de manière portable). Le type de fichier MLB a été défini, en dehors de la définition de SML, pour y remédier.


Le troisième lien est pour une formalisation de la sémantique du système de module de SML. Cette formalisation n’existe pas dans le standard, et a été réalisée indépendamment dans une thèse.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]

Dernière édition par Hibou le Sam 27 Sep 2014 04:33, édité 2 fois.

Ajout d’un lien

Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Jeu 6 Fév 2014 16:46
Message Re: Les références et annexes
Un commentaire de Robin Milner lui‑même (auteur de la définition de Standard ML '97, avec la participation de Mads Tofte), sur l’avenir de SML, dans lequel il exprime l’idée qu’il faut évoluer à partir de SML, et non‑pas faire évoluer SML.

Source : [Sml-implementers] Developing ML (sourceforge.net/mailarchive). 29 Septembre 2001.

Robin Milner a écrit : 
I've read most of the recent discussion (various people have kindly copied or forwarded messages to me, as I'm not a regular member of the list). It's clear that there is considerable interest in advancing - or advancing from - SML. Andrew's and Bob's categorisations show that the range of topics to look at is multi-dimensional. I agree with those who say that languages evolve. My view, expressed in a joint message with Mads Tofte, is that we need evolution _from_ SML, but not evolution _of_ SML. I want to explain this position. […]


Traduction a écrit : 
J’ai lu le plus gros de la récente discussion (diverses gens m’ont aimablement transmis copie ou fait suivre les messages, vu que je ne suis pas un membre régulier de cette liste de diffusion). Il est clair que beaucoup de monde se montre intéressé de faire évoluer — ou d’évoluer à partir de — SML. Les catégorisations [ndt. il fait référence à une branche de la logique] de Andrew et Bon on montré que la gamme des questions sur lesquelles se pencher, a de multiples dimensions. Je suis d’accord avec ceux/celles qui disent que les langages évoluent. Mon opinion, exprimé conjointement dans un message avec Mads Tofte, et nous avons besoin d’une évolution _à partir_ de SML, et pas d’une évolution _de_ SML. Je souhaites expliquer cette position. […]

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Ven 14 Mar 2014 15:57
Message Re: Les références et annexes
Le premier message était erroné, et a été corrigé. La définition de SML, est celle de 1997, et non‑pas celle de 1990. Je m’étais emmêlé les pinceaux à ce sujet, parce que la version de 1997 n’est pas disponible en ligne, ce qui m’avait fait croire à tord, que la version de 1990, visible partout, était la référence actuelle.

Les liens du premier message ont été corrigés, et j’ajoute celui‑ci sous forme de lien annexe, et comme aperçu de la version de 1997 qui n’est publiquement consultable, même si son prix est assez abordable, et ne la rend pas totalement inaccessible non‑plus.

SML '97 Conversion Guide (smlnj.org).

C’est donc un guide du passage de SML '90 à SML '97, qui donne un aperçu des différences entre les deux, et peut permettre de très grossièrement dériver SML '97 à partir de la référence publiquement disponible, de SML '90.

La page est dite en construction, mais n’y faite pas attention, cette page est déjà ancienne, et cela fait des années qu’elle affiche ce message.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Lun 21 Juil 2014 19:56
Message Re: Les références et annexes
SML ne fourni pas de support pour Unicode, ni dans la librairie de base, dans sa syntaxe qui n’accepte pas les noms composés de caractères en dehors de jeu de caractères ASCII de base. C’est probablement une conséquence de l’ancienneté du standard SML, qui date de 1997, qui était une révision d’un standard de 1990.

Unicode (mlton.org).

La librairie de base de MLton inclus une structure WideChar. Comme dit le document, c’est le seul support fourni.

Il fait référence à des discussions à ce propos :

[MLton] WideChar? (mlton.org). Décembre 2004. L’index du sujet est ici : thread.html#26396 (mlton.org).

[MLton] WideChar (mlton.org). Décembre 2004. Le titre n’est plus une question, car le sujet est un résumé de la précédente discussion. L’index du sujet est ici : thread.html#26440 (mlton.org).

[MLton] Unicode / WideChar. Novembre 2005. C’est à propos d’un début d’implémentation dans MLton. L’index du sujet est ici : thread.html#28300 (mlton.org).

En soulignant bien que ceci est en dehors de la définition standard. Cette entorse est compréhensible, vu que le standard n’évolue plus, on ne pas toujours renvoyer à celui‑ci quand une nécessité se fait sentir.
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Sam 27 Sep 2014 04:31
Message Re: Les références et annexes
le système de module n’est pas formalisé par le standard de SML, il y est seulement décrit. La sémantique du système de module a été formalisé indépendamment dans une thèse en 2010 : A true higher-order module system (smlnj-gforge.cs.uchicago.edu) [PDF], George Kuan, 2010.

Ce lien est ajouté au message listant les références hors‑standard.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Jeu 30 Mar 2017 13:28
Message Re: Les références et annexes
La définition d’une future version de la spécification du successeur de SML, nommé sML, est sur GitHub depuis un an environ : Successor-ML (github.com).

Cette définition est basée sur SML 97, et est donc aussi une manière de lire la version 1997 du standard. Cette mise en ligne et cette modification de SML 97, a été autorisée par les ayants droits.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17312
Sam 23 Mar 2019 22:38
Message Re: Les références et annexes
À côté de Successor ML, il a existé Mini ML, défini en 1986 : A simple applicative language: Mini‑ML (inria.fr), Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, Gilles Kahn, 1986.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet