1. Index du forum
  2. Sciences
  3. Sciences Classiques
  4. SML
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.

Un type entier naturel (nat) pour SML
Auteur Message
Hibou
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22324
Dim 9 Fév 2014 20:04
Message Un type entier naturel (nat) pour SML
D’un point de vue mathématique, l’ensemble ℕ des entiers naturels, est un sous‑ensemble de ℤ, l’ensemble des entiers relatifs, et on a ℕ ⊂ ℤ.

D’un point de vue informatique, les entiers peuvent être soit signés, non‑signés, en arithmétique modulo n, ou sans modulo (avec erreur de débordement, le cas échéant).

D’un point de vue informatique toujours, un ensemble n’est jamais infini, et typiquement, il occupe un espace de n bits, dont le cardinal est au plus 2 ^ n. Soit on a alors un ensemble d’entiers naturels, inclus dans l’ensemble d’entiers relatifs et qui n’occupe alors pas tous les n bits qu’il pourrait occuper, soit on a un ensemble d’entiers naturels qui occupe tout l’espace de n bits qu’il peut occuper, mais qui ne respecte plus la relation ℕ ⊂ ℤ (ils sont cependant en intersection, et le cardinal de cette intersection, est 2 ^ n-1).

C’est dit pompeusement (mais formellement), et voici une formulation plus courante que les gens concernés reconnaitront : sur une machine 32 bits, si les entiers relatifs occupent 32 bits, et si les entiers naturels sont inclus dans les entiers relatifs, alors les entiers naturels ne peuvent pas occuper 32 bits, et on perd des entiers naturels, car on borne leur intervalle pour pouvoir les inclure dans les entiers relatifs. Si on préfère ne pas perdre des entiers naturels, alors on peut leur allouer un espace de 32 bits, mais alors ils ne peuvent plus être tous inclus dans l’ensemble des entiers relatifs, car le plus grand entier naturel pouvant être représenté, sera plus grand que le plus grand entier relatif pouvant être représenté.

Le langage Ada opte pour la première solution. C’est mathématiquement correcte, mais techniquement dommage, car quand on doit pouvoir travailler avec des entiers naturels sur 32 bits, on a pas d’autre choix que se rabattre sur les types modulo 2 ^ 32, qui ne correspondent plus mathématiquement aux entiers naturels, dont l’arithmétique n’est pas en modulo n.

Avec SML, c’est encore plus décevant, car le standard du langage ne prévoit simplement pas de type pour les entiers naturels, et seulement un type pour les entiers relatifs, et c’est alors dans tous les cas que l’on doit se rabattre sur le type modulo, d’ailleurs unique (SML a un vocabulaire pauvre, comparé à Ada, pour la spécification des types numériques).

Comme je supporte difficilement d’utiliser un type `int` quand il s’agit formellement d’un type `nat`, j’ai créé une signature et une structure naïve, mais fonctionnelle (sans jeux de mot, lol), offrant un type `nat`. Pour les raisons présentées plus haut, ce type `nat` n’est pas un sous‑ensemble du type `int`. L’inconvénient, ce sont les conversions nécessaires entre `int` et `nat` ; mais c’est à mon avis moins dommage que de perdre des entiers naturels ou que d’utiliser un type modulo.

Dans le message suivant, est rapporté l’intégralité d’un source SML pas très long, pour une signature `NATURAL` et une structure `Nat` l’implémentant. Je ne répète pas les autres commentaires faits dans cette source SML.

Remarque : il n’y a pas encore de colorisation pour SML, et je l’ajouterai un jour prochain.
Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Hibou
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22324
Dim 9 Fév 2014 20:04
Message Re: Un type entier naturel (nat) pour SML

Code : 

(*
   Proposal of a`nat` type for either Successor ML or the Basis Library
   ====================================================================

   A `nat` is a bit like a `word`, it's unsigned, except it's not subject to
   modulo arithmetic, so a `word` is not really nice where `nat` is expected.
   It's a bit like an `int`, except it's never negative, so an `int` is
   neither really nice where a `nat` is expected. These are the reasons why
   a proper `nat` (unsigned and no modulo arithmetic) would be nice.

   Signature `NATURAL` defined below, is mostly the same as that of `INTEGER`,
   with these differences:

     * `toLarge` and `fromLarge` are not defined (although it could be);
     * there is no `minNat`, as it's always zero by definition;
     * there is no `quot` or `rem`, as `nat` is unsigned;
     * there is no `~`, `abs`, `sign` or `sameSign`, as `nat` is unsigned;
     * there are named values for 0, 1, 2 and 3 (more on this below);
     * there are `succ` and `pred` functions (more on this below).

   The named values for most common literals, ranging from 0 to 3, are
   useful due to the lack of proper syntax support for a type `nat`. For other
   literal values, `Nat.fromInt` can be used. A syntax for `nat` should either
   be like for `int`, just with no sign or like for `word`, just with no `0w`
   prefix.

   The functions `succ` and `pred` have two rationales. Like above, it too
   help to deal with the lack of proper syntax support, avoiding direct
   reference to `Nat.one`. Additionally, it match the typical functional
   definition of `nat`, except from this point of view, `succ` should be
   `Succ`, a constructor, while here, it is a function.

   The implementation could either be based on `Int` or `Word`. The naive one
   (and the one I'm using) provided here, in based on `Word`.

   Unfortunately, `open Nat` is not that nice, as there is no overloading
   for the common operations, which shadows that of `int` and `word`.

   2014-02-09

 *)

signature NATURAL =

   sig

      eqtype nat;

      val zero:  nat;
      val one:   nat;
      val two:   nat;
      val three: nat;

      val toInt   : nat -> Int.int;    (* May raise `Overflow` *)
      val fromInt : Int.int -> nat;    (* May raise `Domain`   *)

      val precision : Int.int option;
      val maxNat : nat option;

      val succ: nat -> nat;            (* May raise `Overflow` *)
      val pred: nat -> nat;            (* May raise `Domain`   *)

      val + : nat * nat -> nat;        (* May raise `Overflow` *)
      val - : nat * nat -> nat;        (* May raise `Domain`   *)
      val * : nat * nat -> nat;        (* May raise `Overflow` *)
      val div : nat * nat -> nat;      (* May raise `Div`      *)
      val mod : nat * nat -> nat;      (* May raise `Div`      *)

      val compare : nat * nat -> order;
      val <  : nat * nat -> bool;
      val <= : nat * nat -> bool;
      val >  : nat * nat -> bool;
      val >= : nat * nat -> bool;

      val min : nat * nat -> nat;
      val max : nat * nat -> nat;

      val fmt      : StringCvt.radix -> nat -> string;
      val toString : nat -> string;

      val scan : StringCvt.radix
                    -> (char, 'a) StringCvt.reader
                       -> (nat, 'a) StringCvt.reader;

      val fromString : string -> nat option;

   end; (* NATURAL *)

structure Nat :> NATURAL =

   struct

      structure Word = SysWord;

      type nat = Word.word;

      val zero  = 0w0;
      val one   = 0w1;
      val two   = 0w2;
      val three = 0w3;

      val maxNat = Word.- (0w0, 0w1);
      val maxInt = Word.>> (maxNat, 0w1);

      val succ: nat -> nat =
         fn n =>
            if n = maxNat then raise Overflow
            else Word.+ (n, 0w1);

      val pred: nat -> nat =
         fn n =>
            if n = 0w0 then raise Domain
            else Word.- (n, 0w1);

      val toInt : nat -> Int.int =
         fn n =>
            if maxInt < n then raise Overflow
            else Word.toInt n;

      val fromInt : Int.int -> nat =
         fn i =>
            if Int.< (i, 0) then raise Domain
            else Word.fromInt i;

      val precision : Int.int option = SOME (Word.wordSize);
      val maxNat : nat option = SOME maxNat;

      val op + : nat * nat -> nat =
         fn (x, y) =>
            let val r = Word.+ (x, y);
            in
               if Word.< (r, x) orelse Word.< (r, y) then raise Overflow
               else r
            end;

      val op - : nat * nat -> nat =
         fn (x, y) =>
            if x < y then raise Domain
            else Word.- (x, y);

      val op * : nat * nat -> nat =
         fn (x, y) =>
            if y = 0w0 then 0w0
            else
               let
                  val n = Word.* (x, y);
                  val d = Word.div (n, y);
                  val m = Word.mod (n, y);
               in
                  if d <> x orelse m <> 0w0 then raise Overflow
                  else n
               end;

      val op div : nat * nat -> nat =
         fn (x, y) =>
            if y = 0w0 then raise Div
            else Word.div (x, y);

      val op mod : nat * nat -> nat =
         fn (x, y) =>
            if y = 0w0 then raise Div
            else Word.mod (x, y);

      val compare : nat * nat -> order = Word.compare;
      val op <  : nat * nat -> bool = Word.<
      val op <= : nat * nat -> bool = Word.<=;
      val op >  : nat * nat -> bool = Word.>
      val op >= : nat * nat -> bool = Word.>=;

      val min : nat * nat -> nat = Word.min;
      val max : nat * nat -> nat = Word.max;

      val fmt      : StringCvt.radix -> nat -> string = Word.fmt;
      val toString : nat -> string = fmt StringCvt.DEC;

      val scan : StringCvt.radix
                    -> (char, 'b) StringCvt.reader
                       -> (nat, 'b) StringCvt.reader =
         fn radix =>
            fn getc =>
              (fn strm =>
                  case Int.scan radix getc strm of
                     NONE => NONE
                   | SOME (i, x) =>
                        if Int.< (i, 0) then NONE
                        else SOME (fromInt i, x));

      val fromString : string -> nat option =
         StringCvt.scanString (scan StringCvt.DEC);

   end; (* Nat *)

open Nat;
Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Hibou
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 22324
Lun 10 Fév 2014 10:12
Message Re: Un type entier naturel (nat) pour SML
Mauvaise surprise avec Poly/ML, interpréteur pour lequel sur une machine 32 bits, le type `word` est malheureusement sur 31 bits, ce qui lève une exception `Overflow` avec tous les calculs impliquant des entiers naturels nécessitant 32 bits.

Il est possible de le constater avec ce petit test :

Code : 

val a = 0wxFF;
val b = 0wx100;

val w = a;
print (Word.toString w ^ "\n");
(* OK: prints `FF` *)

val w = w * b + a;
print (Word.toString w ^ "\n");
(* OK: prints `FFFF` *)

val w = w * b + a;
print (Word.toString w ^ "\n");
(* OK: prints `FFFFFF` *)

val w = w * b + a;
print (Word.toString w ^ "\n");
(* Oops: prints `7FFFFFFF` instead of `FFFFFFFF` *)


Et effectivement :

Code : 

print (Int.toString Word.wordSize ^ "\n");
(* Prints `31`... too bad :-( *)


Le compilateur MLton ne souffre pas de cette désastreuse limitation.

Il est heureusement possible de rendre la structure `Nat` concrètement utilisable, en implémentant `nat` avec `SysWord.word` au lieu de `word`. Le second message a été mis à jour en conséquence.

Pour Poly/ML, sur une machine 32 bits, `SysWord.wordSize` vaut bien 32. Un peu étonnement car il n’a pas la nécessité d’en faire autant, pour MLton sur la même machine 32 bits, `SysWord.wordSize` vaut 64 alors que `Word.wordSize`, y vaut 32 et aurait été suffisant, comme l’indique une référence de la librairie standard de base de SML :

The WORD signature (standardml.org)

standardml.org a écrit : 
The type SysWord.word is guaranteed to be large enough to hold any unsigned integral value used by the underlying system.


MLton fait plus que le nécessaire sur ce point. Ça peut tout‑de‑même ne pas être une bonne chose en tous‑points, car des mots non‑natifs, de 64 bits, sur une machine 32 bits, nécessitent plus de traitement. Ce n’est pas très grave pour les additions et soustractions, mais il y a sûrement une pénalité non‑négligeable pour les multiplications, et encore plus pour les divisions et modulos.
Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
  1. Index du forum
  2. Sciences
  3. Sciences Classiques
  4. SML
Heures au format UTC [ Heure d’été ]
cron