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 ?