Una buona informazione sui sistemi di tipo sulla base di contratti / vincoli?

Question

Problema:

Cerco buona introduzione sui sistemi di Tipo , che si basano su contratti / vincoli
(mi dispiace, non mi ricordo che un termine è appropriato per un sistema di tipo) .

Ho bisogno che le informazioni per essere in grado di implementare un sistema di tipo sperimentale di questo tipo.

Per quanto ne so, questo sistema tipo viene utilizzato in XSD (XML Schema Definition).

Invece di definire un tipo di dati, si definisce vincoli sul set di valori possibili.

Esempio:

Mi definisco un metodo con un parametro, che è o "nothing", o corrispondente al campo [0..100] integrale.

Tale metodo avrebbe accettato i seguenti valori:

"nothing"
0
1
...
100

Spero, avrei potuto fare la mia auto chiaro.

Answer 1

Common Lisp offre tale tipo di test a tempo di esecuzione . Ha un sistema di tipo elaborato, ma non è usato come si potrebbe essere abituati a in un linguaggio staticamente tipizzato. Il check-type accetta un typespec , che può essere una specifica incorporato o quello definito dalla macro deftype . I vincoli esprimibili con typespecs sono quelle di una funzione predicato scritto nella lingua del paese ospitante, vale a dire che tutto ciò che è possibile ispezionare un tempo di esecuzione può essere i criteri per ciò che costituisce il nuovo tipo.

Si consideri questo esempio:

(defun is-nothing (val)
  (when (stringp val)
    (string= val "nothing")))

(deftype strange-range ()
  "A number between 0 and 100 inclusive, or the string \"nothing\"."
  '(or (integer 0 100)
       (satisfies is-nothing)))

che definisce un tipo chiamato "strano-range". Ora testare alcuni valori contro di essa:

CL-USER> (let ((n 0))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 100))
           (check-type n strange-range))
NIL
CL-USER> (let ((n "nothing"))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 101))
           (check-type n strange-range))

L'ultimo innesca il debugger con il seguente messaggio:

The value of N should be of type STRANGE-RANGE.
The value is: 101
   [Condition of type SIMPLE-TYPE-ERROR]

Questo provoca lo stesso risultato:

CL-USER> (let ((n "something"))
           (check-type n strange-range))

I vincoli può imporre in questo modo sono espressive, ma non servono allo stesso scopo che i sistemi di tipo elaborati di linguaggi come Haskell o Scala fanno. Mentre definizioni del tipo possono indurre il compilatore Common Lisp per emettere il codice più su misura per ed efficiente per i tipi degli operandi, gli esempi di cui sopra sono più di un modo conciso di scrivere i controlli di tipo run-time.

Answer 2

Si può avere uno sguardo a linguaggi come Haskell , o anche Agda . Inoltre, Oleg ha un sacco di grandi risorse.

Answer 3

Questa non è la mia area di competenza, quindi potrebbe essere fuori tema, ma Microsoft Research ha un progetto noreferrer Code Contracts , che 'forniscono un modo indipendente dal linguaggio per esprimere le ipotesi di codifica in programmi .NET. I contratti assumono la forma di precondizioni, postcondizioni e invarianti degli oggetti' .