Terminologia corretta nella teoria dei tipi: tipi, costruttori di tipi, tipi / tipi e valori

Bene, andiamo uno alla volta.

Valori

I valori sono i pezzi di dati concreti che i programmi valutano e manipolano. Niente di speciale, alcuni esempi potrebbero essere

• 1
• true
• "fizz buzz foo bar"

Tipi

Una bella descrizione per un tipo è "un classificatore per un valore". Un tipo è un po 'di informazioni su quale sarà il valore in fase di esecuzione, ma indicato al momento della compilazione.

Ad esempio, se mi dici che e : bool al momento della compilazione, e saprò che e è o true o false durante il runtime, nient'altro! Poiché i tipi classificano i valori in modo simile, possiamo utilizzare queste informazioni per determinare alcune proprietà di base del tuo programma.

Ad esempio, se mai ti vedessi aggiungere e e e' quando e : int e e' : String , allora so che qualcosa è un po 'spenta! In effetti posso segnalare questo e lanciare un errore al momento della compilazione, dicendo "Ehi, non ha alcun senso!".

Un sistema di tipi più potente consente tipi più interessanti che classificano valori più interessanti. Ad esempio, consideriamo alcune funzioni

f = fun x -> x

È abbastanza chiaro che f : Something -> Something , ma che cosa dovrebbe essere Something ? In un noioso sistema di tipi, dovremmo specificare qualcosa di arbitrario, come Something = int . In un sistema di tipi più flessibile, potremmo dire

f : forall a. a -> a

Vale a dire "per ogni a , f esegue il mapping di a a a ". Usiamo f in generale e scriviamo programmi più interessanti.

Inoltre, il compilatore controllerà effettivamente il classificatore che gli abbiamo dato, se f = fun x -> true avremo un bug e il compilatore lo dirà!

Quindi come tldr; un tipo è un vincolo di tempo di compilazione sui valori che un'espressione può essere in fase di runtime.

Tipo Costruttore

Alcuni tipi sono correlati. Ad esempio, un elenco di numeri interi è molto simile a un elenco di stringhe. Questo è quasi come sort per interi è quasi come sort per le stringhe. Possiamo immaginare una sorta di fabbrica che costruisce questi tipi quasi identici generalizzando le loro differenze e costruendole su richiesta. Questo è ciò che un costruttore di tipi è. È un po 'come una funzione da tipi a tipi, ma un po' più limitata.

L'esempio classico è un elenco generico. Un costruttore di tipi è solo la definizione generica

 data List a = Cons a (List a) | Nil

Ora List è una funzione che associa un tipo a a un elenco di valori di quel tipo! In Java-land penso che questi siano chiamati "classi generiche"

Parametri tipo

Un parametro di tipo è solo il tipo passato a un costruttore di tipo (o funzione). Proprio come nel livello del valore, diciamo che foo(a) ha un parametro a proprio come List a ha un parametro di tipo a .

Tipi

I tipi sono un po 'complicati. L'idea di base è che alcuni tipi sono simili. Ad esempio, abbiamo tutti i tipi primitivi in java int , char , float ... che si comportano tutti come se avessero lo stesso "tipo". Tranne che quando parliamo dei classificatori per i tipi stessi, chiamiamo i tipi di classificatori. Quindi int : Prim , String : Box , List : Boxed -> Boxed .

Questo sistema fornisce belle regole concrete su quale tipo di tipi possiamo usare dove, proprio come i tipi governano i valori. Sarebbe chiaramente una sciocchezza dire

 List<List>

o

 List<int>

In Java poiché List deve essere applicato a un tipo concreto da utilizzare in questo modo! Se guardiamo i loro tipi List : Boxed -> Boxed e dal Boxed -> Boxed /= Boxed , quanto sopra è un errore gentile!

La maggior parte delle volte non pensiamo davvero ai generi e li consideriamo semplicemente come "buon senso", ma con sistemi di tipo più elaborati è importante pensarci.

Un piccolo esempio di ciò che ho detto finora

 value   : type : kind  : ...
 true    : bool : Prim  : ...
 new F() : Foo  : Boxed : ...

Migliore lettura di Wikipedia

Se sei interessato a questo genere di cose, ti consiglio vivamente di investire un buon libro di testo. La teoria dei tipi e il PLT in generale sono piuttosto vasti e senza una base coerente di conoscenza tu (o almeno io) puoi andare in giro senza arrivare da qualche parte per mesi.

Due dei miei libri preferiti sono

• Tipi e linguaggio di programmazione - Ben Pierce
• Fondamenti pratici dei linguaggi di programmazione - Bob Harper

Entrambi sono libri eccellenti che introducono ciò di cui ho appena parlato e molto altro in dettagli belli e ben spiegati.

How are these things defined properly?

Sono correttamente definiti da un rigido supporto accademico matematico, che fornisce forti asserzioni su ciò che sono, su come funzionano e su ciò che è garantito.

Ma i programmatori in gran parte non hanno bisogno di saperlo. Hanno bisogno di capire i concetti.

Valori

Iniziamo con i valori, dal momento che tutto si costruisce da lì. I valori sono i dati utilizzati nel calcolo. A seconda dell'approccio, sono i valori con cui tutti hanno familiarità: 42, 3.14, "Come ora marrone mucca", il record personale di Jenny in Contabilità, ecc.

Altre interpretazioni dei valori sono simboli . La maggior parte dei programmatori comprende questi simboli come "valori" di un'enumerazione. Left e Right sono simboli per l'enum Handedness (ignorando persone e pesci ambidestri).

Indipendentemente dall'implementazione, i valori sono le diverse cose con cui la lingua lavora per eseguire i calcoli.

Tipi

Il problema con i valori è che non tutti i calcoli sono legali per tutti i valori. 42 + goat non ha davvero senso.

È qui che entrano in gioco i tipi. I tipi sono metadati che definiscono sottoinsiemi di valori. Il Handedness enum sopra è un buon esempio. Questo tipo dice "solo Left e Right possono essere usati qui". Ciò consente ai programmi di determinare molto presto che determinate operazioni causeranno errori.

Un altro uso pratico da considerare è che sotto il cofano, i computer lavorano con i byte. Il byte 42 potrebbe significare il numero 42, o potrebbe significare il carattere *, o potrebbe significare Jenny da Contabilità. Anche i tipi (nell'uso pratico, non teorico) aiutano a definire la codifica per la raccolta sottostante di byte utilizzati dai computer.

Tipi

Ed ecco dove iniziamo ad andare un po 'là fuori. Quindi, quando un linguaggio di programmazione ha una variabile che si riferisce a un tipo, che tipo ha ha?

Ad esempio, in Java e C # ha il tipo Type (che ha il tipo Type , che ha ... e così via fino in fondo). Questo è il concetto alla base di tipi . In alcune lingue, puoi fare cose un po 'più utili con una variabile Type di Java e C #. Quando ciò accade, diventa utile dire "Voglio un valore che è un tipo, ma è anche un po ' tipo di IEnumerable<int> ". Ta-da! Tipi.

La maggior parte dei programmatori può pensare a tipi come i vincoli generici di Java e C #. Considera public class Foo<T> where T: IComparable{} . In una lingua con tipi, la dichiarazione della variabile T: kindOf(IComparable) diventa legale; non solo una cosa speciale che puoi fare nelle dichiarazioni di classe e di funzione.

Type Constructors

Forse non sorprendentemente, i costruttori di tipo sono semplicemente costruttori per i tipi . "Ma come si costruisce un tipo? I tipi solo sono .". Eh ... non tanto.

Inoltre, non sorprende che sia abbastanza difficile creare tutti i diversi sottoinsiemi di valori utili che qualsiasi programma di computer userà mai. I costruttori di tipo funzionano per consentire ai programmatori di "costruire" questi sottoinsiemi in modi significativi.

L'esempio più onnipresente di un costruttore di tipi è una definizione di array: int[4] . Qui stai specificando 4 al costruttore del tipo, che usa il valore per creare un array di int s con 4 voci. Se hai specificato un tipo di input diverso, otterrai un tipo di output diverso.

I generici sono un'altra forma di costruttore di tipi, che accetta un altro tipo come input.

In molte lingue esiste un costruttore di tipi come P -> R per creare un tipo che rappresenta una funzione che accetta il tipo P e restituisce il tipo R .

Ora il contesto determinerà se una "funzione che restituisce un tipo" è un costruttore di tipi o meno. Nella mia esperienza (dichiaratamente limitata), la linea è "puoi usare questo tipo al momento della compilazione?". Sì? Tipo costruttore. No? Solo una funzione.

Tipo parametro

Quindi ti ricordi i parametri passati a Type Constructors? Sono comunemente noti come parametri di tipo, poiché la forma comune di un costruttore di tipo è Type[param] o Type<param> .