Ce type ne me revient pas !

Qu'est qu'un système de type ?

  • Meta information attachée à une structure du langage
  • Variable, fonction, expression ou module

Un type défini l'ensemble des valeurs possibles

//Attention code Groovy, parce que ca ressemble à Java en plus court !

//Type COLOR, 3 valeurs possibles
enum COLOR {
    RED, BLUE, YELLOW
}

// Type Name, une infinité de valeur possibles
class Name {
    String value
}

Un type défini quelles sont les opérations qui lui sont applicables


class Name {
    String value

    //Définition "interne"
    Name lordify() {
         return new Name(value:'sir ' + this.value)
    }
}

class Lordificator {

      //Définition "externe"
      static Name lordify(Name name) {
          return new Name(value:'sir ' + name.value)
      }
}

Un type défini la façon dont est stockée la donnée


                        Float in32bit = 6.5f // sur 32 bits
                        Double in64bit = 6.5 // sur 64 bits

Un type défini le sens de la donnée


class Person {
     //Plus de sens qu'une simple String
     //Car on peut de cette façon limiter les opérations faisables
     Name name
}

Pourquoi un système de type ?

  • Définir des interfaces entres les "morceaux" d'un programme
  • Ainsi diminuer les bugs en s'assurant que les morceaux sont connectés de façon cohérente
  • Lisibilité
  • Optimisations

La vérification de type peut se faire

  • Au moment de la compilation (vérification statique)
  • Au moment de l'exécution (vérification dynamique)

Le typage statique

Un système de typage statique pour un langage Turing-Complet doit :

  • être "sound" : rejeter les programmes invalides
  • être décidable : il est possible d'écrire un algorithme déterminant si le programme est bien typé

Limite du typage statique

  • il est toujours possible d'écrire un programme "juste" mais qui sera rejeté par le compilateur (la preuve dérive du theorème d'incomplétude de Gödel)
  • Certaines fonctionnalités ne peuvent pas être vérifiées (downcasting, par exemple)

Java n'a pas un compilateur très puissant


//Ne compile pas
public class Exemple {
    static Integer getIntOrZero(Object obj) {
        if (obj instanceof Integer) {
            return obj;
        } else {
            return 0;
        }
    }
}

Quelques langages statiquement typés

  • Java
  • Scala
  • Ceylon
  • Kotlin
  • C
  • C++
  • Haskell

Le typage dynamique

  • La vérification de la validité du programme se fait à l'exécution

Apport du typage dynamique : le Dynamic Dispatch

class Human {}

class Troll extends Human {}

public class Main {
    public static void speak(Human h) {
        System.out.println("Raconte des choses passionantes");
    }

    public static void speak(Troll h) {
        System.out.println("Emacs c'est nul comparé à vim");
    }

    public static void main(String[] args) {
        Human h = new Troll();
        speak(h);
        // En Java : la phrase d'humain normal
        // En groovy : la phrase de troll
    }
}

Apport du typage dynamique :Late Binding

  • Late Binding = objet sur lequel on appelle la méthode
  • Dynamic dispatch = quelle méthode on appelle
  • N'existe donc pas vraiment Java

function makeTheDuckQuack(duck) {
     //Ici le type de duck est inconnu,
     //On ne le connaitra qu'à l'execution
     duck.quack();
}

Apport du typage dynamique :la réflexion

  • Pour pouvoir faire de la réflexion il faut connaitre les types au runtime !

Mais en Java, on peut faire de la réflexion !

C'est un langage à typage statique, non ?

Aspect Hybride

  • La grand majorité des langages modernes à typage statique ont aussi une partie dynamique

public Integer castToInt(Number num) {
        return (Integer) num;
}
//Le code ci-dessus renvoie une ClassCastException
//si le type de num n'est pas Integer
//Le type de num est donc accessible et vérifié au runtime !

Quelques langages mettant en avant le typage dynamique

  • Groovy
  • Clojure
  • JavaScript

Static vs Dynamic

  • Détection au plus tôt des bugs de type...
  • ... même si ces bugs n'arrivent que rarement
  • Oui, mais tous les bugs peuvent être considérés comme des erreurs de type...
  • ... du moment que l'on utilise un langage avec un système de type suffisament puissant

Static vs Dynamic

  • Le typage statique permet au compilateur de faire des optimisations...
  • ... certains langages dynamiques permettent donc des annotations pour aider le compilateur
  • Le typage dynamique permet au compilateur d'être plus rapide et de recharger à chaud ce qui diminue le temps de cycle

Static vs Dynamic

  • La déclaration de type sert de documentation dans le code...
  • ... mais sans inférence de type, elle diminue la lisibilité

Static vs Dynamic

  • Les langages dynamiques permettent la metaprogrammation...
  • ... meme si certains langages statiques possèdent des API de réflexion

Enfonçons le clou

  • Un langage à typage dynamique impose que ses structures aient un type !
  • Il y a donc bien des types en JS et PHP
  • ASM, Brainfuck ou Whitespace sont des langages sans types

Typage explicite vs implicite

//Java
String explicit = "je suis explicitement une string";

//Scala
val implicit = "je suis implicitement une string"
                    
-- haskell
let add x y = x + y
:info add
-- renvoie add :: Num a => a -> a -> a
-- l'utilisation de + a permis de typer implicitement les paramètres de add

Interlude

le typage faible et le typage fort

Un langage aurait un typage plus faible qu'un autre si :

  • Il permet les conversions implicites
  • Il permet l'arithmétique sur les pointeurs
  • Il ne compile pas statiquement
  • Il compile statiquement mais permet les erreurs de type au runtime

Exemple de langage fortement typé : JavaScript


var aNumber = 3;
function add(a, b) {
    return a + b;
}

Exemple de langage faiblement typé : Scala


def isNegative(x:Number):Boolean = x.asInstanceOf[Float] < 0.0

Fin de l'interlude

  • Toujours préférer d'autres termes que fort & faible
  • Sauf si l'objectif est d'envenimer un débat

Le typage structurel

  • La compatibilité de type est donnée par la structure et non par une déclaration explicite
  • Par opposition au système de type nominatif

Exemple en TypeScript


interface Point {
    x:number
    y:number
}

function printPoint(p:Point) {
    console.log('('+p.x+','+p.y+')')
}

printPoint({x:1, y:2})

Quelques langages typés structurellement

  • Haskell
  • OCaml
  • TypeScript
  • Dart
  • Scala*

Le Duck Typing

  • Typage structurel appliqué aux langages dynamiques
  • Si ca marche comme un canard, nage comme un canard et caquette comme un canard, alors c'est un canard

Exemple en ES6

function makeTheDuckQuack(duck) {
    duck.quack();
}

class Duck {
    quack() {
        console.log('coin coin');
    }
}

class Unicorn { }

makeTheDuckQuack(new Duck()); //coin coin

var unicorn = new Unicorn();
unicorn.quack = function() { console.log('COIN COIN'); };
makeTheDuckQuack(unicorn); // COIN COIN

makeTheDuckQuack(new Unicorn()); // type error

Quelques langages incluant Duck Typing

  • Clojure
  • JavaScript
  • Groovy

Le futur

Le typage graduel

  • Permet au développeur de typer au choix à la compilation ou à l'execution
  • Souvent confondu avec le typage optionnel (qui permet de désactiver le type checking)
  • Utilisation d'un type joker any

Pourquoi TypeScript est presque réellement graduellement typé


function display(y : string) {
    document.body.innerHTML = y.charAt(0);
    // error au runtime: charAt is undefined, pas de check du type au runtime
}

var x : any = 3;
display(x);

Le typage dépendant

Un "type dépendant" est un type dépendant d'une valeur définie

Exemples

  • Un Type "Nombre Entier compris entre 0 et n"
  • Un type List indiquant la taille de la liste
  • Un type Matrix indiquant la hauteur et la largeur de la matrice

Exemples de languages implémentant les types dépendants

  • Idris
  • Agda
  • Coq
  • Scala*

Exemples (en Idris)


Vect.index 2 [3,4,5] -- renvoit 5
Vect.index 3 [3,4,5] -- ne compile pas


-- [3, 4, 5] est de type Vect 3 Integer

Des questions ?