Qual è la relazione tra tipi non chiusi e rigore?

Question

I tipi non condivisi, come Int#, e le funzioni rigorose, come f (!x) = ..., sono qualcosa di diverso, ma vedo una somiglianza concettuale - in qualche modo impediscono i thunk/la pigrizia. Se Haskell fosse un linguaggio rigoroso come Ocaml, ogni funzione sarebbe rigorosa e ogni tipo unboxed. Qual è la relazione tra i tipi non condivisi e l'applicazione della severità?

Answer 1

Unboxed vs Boxed dati

Per sostenere parametric polymorphism e laziness, per i tipi di dati Haskell predefinite sono rappresentati in modo uniforme come un puntatore a un closure su the heap, con una struttura come questa:

Questi sono valori "in scatola". Un unboxed oggetto è rappresentato direttamente dal valore stesso, senza alcuna indiretta o chiusura. Int è in scatola, ma Int# è unbox.

valori Lazy richiedono una rappresentazione in scatola. I valori rigorosi non lo sono: possono essere rappresentati come chiusure pienamente valutate nell'heap o come primitive strutture unboxed. Notare che pointer tagging è un'ottimizzazione che è possibile utilizzare su oggetti boxed per codificare il costruttore nel puntatore alla chiusura.

Il rapporto di rigore

Normalmente, i valori disimballati sono generati in un modo ad hoc dal compilatori funzionali. In Haskell, tuttavia, lo unboxed values è speciale.Essi:

1. hanno un tipo diverso, #;
2. può essere utilizzato solo in luoghi speciali; e
3. non sono sollevati, quindi non sono rappresentati come puntatori a un valore di heap.

Poiché non sono sollevati, sono necessariamente rigidi. La rappresentazione della pigrizia non è possibile.

Così tipi particolari non in scatola, come Int#, Double#, sono rappresentati proprio come doppio o int sulla macchina (in notazione C).

Rigore Analisi

Separatamente, GHC fa strictness analysis dei normali tipi di Haskell. Se l'utilizzo di un valore è rigoroso, ovvero non può mai essere "indefinito", l'ottimizzatore potrebbe sostituire tutti gli usi del tipo normale (ad esempio Int) con uno non registrato (Int#), poiché sa che l'uso di Int è sempre rigoroso, e quindi la sostituzione con il più efficiente (e sempre severo) tipo Int# è sicuro.

Possiamo ovviamente avere tipi severe senza tipi disimballati, ad esempio, un elemento-rigida lista polimorfico:

data List a = Empty | Cons !a (List a) 

è severo nei suoi elementi, ma non li rappresentano come valori senza custodia.

Questo segnala anche l'errore che avete fatto riguardo alle lingue severe, like OCaml. Devono ancora supportare il polimorfismo, quindi forniscono una rappresentazione uniforme o specializzano tipi di dati e funzioni per ogni tipo. GHC di default usa la rappresentazione uniforme, come fa OCaml, anche se GHC può anche specialize types and functions ora (come i modelli C++).

Answer 2

I tipi non in scatola sono necessariamente rigidi, ma non tutti i valori rigorosi sono necessariamente unbox.

data Foo a = Foo !a !a 

ha due campi severe

data Bar a = Bar {-# UNPACK #-} !Int !a 

ha due campi severe, ma il primo è unboxed.

In definitiva, il motivo per cui i tipi non condivisi sono (necessariamente) rigidi è che non vi è posto per archiviare il thunk in quanto sono dati semplici e stupidi a quel punto.

Answer 3

Argomenti di qualsiasi tipo può essere fatta "rigida", ma gli unici tipi disimballati che sono corrispondenti tipi scatolari sono Char#, Int#, Word#, Double# e Float#.

Se si conoscono linguaggi di basso livello come C, è più semplice da spiegare. I tipi Unboxed sono come , double, ecc. Ei tipi in scatola sono come int*, double*, ecc. Quando hai uno int, conosci già l'intero valore come viene rappresentato nel modello di bit, quindi, non lo è pigro. Deve essere anche rigoroso, poiché tutti i valori di int sono validi e non ⊥.

Tuttavia, dato un int* è possibile scegliere di dereferenziare il puntatore in un secondo momento per ottenere il valore effettivo (quindi pigro), ed è possibile avere puntatori non validi (contiene ⊥, vale a dire non severi).