Se Scheme non è tipizzato, come può avere numeri e liste?

3

Si dice che lo schema sia solo un'estensione del Calcolo Lambda non tipizzato (correggimi se sbaglio). Se questo è il caso, come può avere liste e numeri? Quelli, per me, sembrano 2 tipi di base. Quindi direi che Racket è in realtà un'estensione del Lambda Calculus Simply Typed. No?

Domanda:

  • Il sistema di tipi di Scheme è effettivamente basato o più simile al Lambda Calculus semplicemente tipizzato o non tipizzato?

  • In che modo differisce da Untyped e / o semplicemente da tipizzazione Lambda Calculus?

(La stessa domanda è valida per linguaggi "non tipizzati" come Python e JavaScript - tutti sembrano avere per me tipi di base.)

    
posta MaiaVictor 29.05.2014 - 22:11
fonte

3 risposte

7

Quando i teorici del tipo dicono "digitato", intendono quello che la maggior parte dei programmatori chiama staticamente digitato . Ciò è dovuto a una divisione fondamentale: i teorici del tipo si prendono cura delle dimostrazioni e delle bestie imparentate e quindi si preoccupano delle affermazioni che si applicano a tutte le possibili esecuzioni di un programma. La semplice nozione di "tag di tipo runtime" non ha senso per loro. Se un teorico del tipo dice "questo ha tipo int " significa "Posso dimostrare formalmente che questo prende sempre solo valori di int ".

Al contrario, una lingua non tipizzata è quella in cui non è possibile creare una tale prova, perché la lingua non fornisce sufficienti garanzie / informazioni. Questo è il significato originale di "non tipizzato" ed è utilizzato attivamente da (una minoranza di) persone che parlano di sistemi di tipi online. Un termine alternativo è "unityped", perché se devi assegnare un tipo, hai solo il tipo banale "qualsiasi valore qualsiasi" disponibile.

Il lambda calculus semplicemente digitato è stato digitato in questo senso, ha un sistema di tipo statico come si potrebbe dire. Nello stesso senso, sia Scheme che il calcolo lambda non tipizzato non sono tipizzati.

I programmatori, d'altra parte, vogliono principalmente sapere che tipo di valore si trova in qualche posizione di memoria; se questa conoscenza è innata nel codice sorgente per un compilatore da esplorare e utilizzare, o se è determinata in fase di esecuzione, è una decisione separata.

Conformemente alla loro comprensione del "tipo", i programmatori hanno una definizione diversa di "non tipizzato": un sistema che ha informazioni statiche né tag di runtime, perché c'è effettivamente solo "un tipo" da scegliere (ad esempio in Tcl, tutto è una stringa). In questo senso, il calcolo lambda non tipizzato è ancora non tipizzato (tutto è una funzione), ma Scheme è, come si nota, digitato (anche se in modo dinamico).

    
risposta data 29.05.2014 - 22:47
fonte
5

Il Lambda Calculus non tipizzato non è tipizzato, perché non si occupa dei tipi. Il Lambda Calculus non tipizzato non è un linguaggio di programmazione pratico, ma semplicemente una base per un pratico linguaggio di programmazione.

Lo schema è tipizzato, perché nel mondo reale dobbiamo memorizzare e manipolare dati reali, piuttosto che simboli matematici. Quel sistema si basa sul calcolo Lambda non tipizzato significa solo che a lui piacciono alcune delle sue caratteristiche.

Se vuoi saperne di più sul sistema di tipi dinamici di Scheme, puoi leggere link

    
risposta data 29.05.2014 - 23:05
fonte
3

La semplice risposta è che Scheme non è untyped: come hai notato, i programmi Scheme possono usare valori di diversi tipi utili. Tuttavia, le persone significano qualcosa quando dicono che Scheme non è tipizzato, significano qualcosa che è meglio esprimere dicendo che Scheme ha un sistema di tipo dinamico. Lasciatemi (eventualmente) spiegare.

Quando le persone dicono "il calcolo lambda non tipizzato", lo chiamano non tipizzato perché tutti i valori con cui si tratta sono dello stesso tipo: combinatori (potreste averli sentiti chiamati anche "funzioni"). Programmare in un linguaggio del genere è pericoloso perché devi tenere a mente che tipo di cosa volevi rappresentare con ogni valore. Il sistema non ha un aiuto integrato per catturare i tuoi errori.

Le persone di lingue effettivamente programmano tendenzialmente [^ 1] di avere più aiuto a distinguere diversi tipi di valori, questo aiuto extra è nella forma di (1) una raccolta più ricca di tipi per i valori di cui la lingua ti permette di parlare e (2) messaggi di errore che si verificano quando si tenta di applicare un'operazione a un valore di un tipo per il quale l'operazione non è definita.

In alcune implementazioni linguistiche, i programmi possono essere compilati o pre-elaborati in qualche modo prima di essere eseguiti. Se ricevi messaggi di errore sull'utilizzo di valori del tipo sbagliato durante questa fase di compilazione, prima di eseguire il programma, si dice che l'implementazione utilizzi la digitazione statica.

Se (1) non c'è una fase di compilazione o pre-elaborazione o (2) c'è ma si ottengono comunque solo messaggi di errore sull'utilizzo di valori del tipo errato durante l'esecuzione del programma, quindi si dice che l'implementazione usi la dinamica digitazione.

La maggior parte (tutte?) le implementazioni dello schema utilizzano un sistema di battitura dinamico. Ci sono linguaggi abbastanza simili a Scheme che hanno un'implementazione usando la tipizzazione statica, come Racket tipizzato.

[^ 1]: ci sono lingue che le persone hanno effettivamente utilizzato per creare software in cui tutti i valori sono essenzialmente dello stesso tipo, come la maggior parte delle lingue delle macchine native del computer, i linguaggi di assemblaggio e BCPL .

    
risposta data 02.06.2014 - 06:10
fonte

Leggi altre domande sui tag