Qual è il comune supertipo di tutte le istanze di tipo nella teoria dei tipi

Question

Sto provando a progettare un'ontologia come potrebbe essere definita con OWL o Topic Maps che include il supporto per tipi polimorfici come Lista [T] dove T è un il parametro type dell'intervallo Kind In (Nothing, Any) e List è il tipo di funzione * -> *. In definitiva, voglio descrivere un'ontologia del sistema di tipi in linguaggio semantico con sufficiente dettaglio e rigore che potrebbe essere la base per un codice software sicuro per tipo scritto nello stesso linguaggio semantico.

Con questo obiettivo in mente, sto cercando di capire una struttura gerarchica di tipi in cui tipo, tipo di intervallo e tipo di funzione sono tutte istanze di tipo. Esiste un nome formale per il comune "super-genere" di tutti i tipi? Il termine migliore che riesco a trovare è "Kind Instance". Questo è anche un concetto significativo nella teoria dei tipi? Anche se non lo fosse, ho bisogno di un tale concetto per dire cose come (nella terminologia di Topic Maps) "un'associazione tipo-argomento-tipo-vincolo ha un Ruolo 'tipo-permesso' il cui lettore deve essere di tipo 'Tipo Istanza '".

Oltre a questo, ho appena iniziato ad insegnare la teoria del tipo per questo progetto e ho ancora molto da imparare prima di poterlo completare. Ho letto alcuni documenti su scala relativi alla teoria dei tipi, tra cui Generics of a Higher Kind (http://adriaanm.github.com/files/higher.pdf) e ho iniziato a lavorare a modo mio attraverso l'astrazione di livello sicuro in Scala (http://adriaanm.github.com/files/scalina-final.pdf) e Type Constructor Polymorphism for Scala[pdf]. Ho meno familiarità con Haskell che con Scala, ma ho incontrato alcuni documenti dall'aspetto rilevante come lo System F with Type Equality Coercions[pdf] che mi servirà una comprensione molto più avanzata di Haskell per capire. Se qualcuno può suggerire una progressione del materiale di lettura per apprendere il sistema di tipi di Haskell a partire dal livello principiante e condurre fino a principi avanzati come i Tipi di dati algebrici generalizzati, sarebbe anche molto apprezzato.

Infine, se siete a conoscenza di tentativi di descrivere un sistema di tipi in un linguaggio di ontologia semantica come OWL o Topic Maps, o se avete suggerimenti su come farlo, mi piacerebbe anche ascoltarlo.

Answer 1

Non c'è introduzione migliore alla teoria del testo di Benjamin Pierce "Tipi e linguaggi di programmazione". Non penso che esistano nomi standardizzati per i livelli sopra il genere, ma "ordinare" è una scelta comune. Un'altra scelta comune è quella di passare direttamente ai tipi dipendenti e appiattire la gerarchia, in modo che ci sia solo un livello dopo tutto. Una regola di digitazione comune da aggiungere in questa situazione (quando si tratta di linguaggi di programmazione giorno per giorno il cui contenuto logico di solito non è così importante) è la regola "Tipo: Tipo", in modo che, ad esempio, 3: Int: Tipo : Tipo: Tipo: ...