Sarei interessato a definire formalmente (e di conseguenza a dimostrare) un "sistema di tipi" per, beh, un sistema di tipi. Più specificamente, vorrei esplorare l'idea di ciò che C ++ chiama concetti per la mia tesi di laurea. Come si dovrebbe definire un tale sistema (formalmente)? È fondamentalmente un meta-linguaggio per la programmazione generica, suppongo, ma tutto il materiale che ho trovato finora è fondamentalmente legato alla sintassi di una programmazione specifica lingua.
L'idea di base è di fornire un'interfaccia per i tipi parametrici.
Ad esempio:
Un argomento per la funzione foo(T) è un po '(sfortunatamente qualsiasi) T. (Questo tipo è noto staticamente .) E, vorrei definire un'interfaccia per tale tipo, in modo che questa T sia effettivamente non qualsiasi T, ma un tipo che è conforme a un'interfaccia, come ad esempio: " Affinché questo tipo sia legale per la funzione foo, deve essere conforme a: Questo e quel concetto / interfaccia per controllare staticamente ".
I concetti definiscono "interfacce" correlate e significative che vincolerebbero il tipo T. Attualmente, il linguaggio C ++ non esegue tali controlli, semplicemente cerca di fare qualunque cosa sia che foo(T) faccia su qualsiasi tipo e spera che funzioni. Se il messaggio di errore non è di lunghezza di un romanzo decente, poiché l'errore viene rilevato troppo tardi e il compilatore deve "sputare" l'intero processo di come è arrivato a un errore.
Alla fine vorrei mostrare il concetto (errm, idea, mi dispiace per l'ambiguità) sul C ++ in particolare, se questo è rilevante.
Grazie,
~ Scarlet