Qual è il WHNF di un newtype e come funziona rseq su un newtype?

Question

Poiché i codici newtype vengono effettivamente rimossi durante la compilazione, non hanno thunk, solo valori. Quindi cosa succede se chiedo il suo WHNF usando rseq? Per esempio in

Sum (lengthyComputation :: Int) `using` rseq 

dove Sum è definito come

newtype Sum a = Sum { getSum :: a } 

sarà lengthyComputation ottenere valutato o no? È specificato/documentato da qualche parte in modo che possa contare su di esso?

---

Aggiornamento: Mi spiego i miei dubbi in modo più dettagliato. Intuitivamente si dice: "newtype è rigoroso, quindi chiaramente il suo WHNF è il WHNF di ciò che è racchiuso all'interno". Ma ritengo che questa sia una scorciatoia molto imprecisa e il ragionamento non è così chiaro. Lasciatemi fare un esempio:

Per i tipi standard data, WHNF può essere definito come una forma in cui è noto quale costruttore è stato utilizzato per la costruzione del valore. Se, per esempio, non abbiamo avuto seq, potremmo creare la nostra

seqMaybe :: Maybe a -> b -> b 
seqMaybe Nothing = id 
seqMaybe _  = id 

e allo stesso modo per qualsiasi tipo data, semplicemente pattern matching su uno dei suoi costruttori.

Ora diamo

newtype Identity a = Identity { runIdentity :: a } 

e creare un simile seqIdentity funzione:

seqIdentity :: Identity a -> b -> b 
seqIdentity (Identity _) = id 

chiaramente, nulla è costretto a WHNF qui. (Dopo tutto, sappiamo sempre quale costruttore è stato utilizzato.) Dopo la compilazione, seqIdentity sarà identico a const id. In effetti, non è possibile creare polimorfo seqIdentity tale da costringere la valutazione di un valore racchiuso all'interno di Identity! Potremmo definire WHNF a di un newtype per essere semplicemente il valore non modificato, e sarebbe coerente. Quindi credo che la domanda sia: come viene definito WHNF per newtype s? O non c'è una definizione rigorosa, e il comportamento "è il WHNF di ciò che è dentro" è semplicemente assunto come qualcosa di ovvio?

Answer 1

Per la sezione sulla Datatype renamings nella relazione,

A differenza di tipi di dati algebrici, il costruttore newtype N è unlifted, in modo che N ⊥ è lo stesso di ⊥.

Qui

Sum ⊥ = ⊥ 

così debole testa normale forma di newtype è la WHNF del tipo avvolto e

Sum (lengthyComputation :: Int) `using` rseq 

valuta lengthyComputation (quando l'intera espressione viene calcolata, una semplice legame

let x = Sum (lengthyComputation :: Int) `using` rseq 

ovviamente no, ma è lo stesso senza il costruttore newtype).

Il defining equations per seq sono

seq ⊥ b = ⊥ 
seq a b = b, if a ≠ ⊥ 

e quindi

seq (Sum ⊥) b = ⊥ 

e in

seq (lengthyComputaton :: Int) b 

il seq è necessario per scoprire (scusate per l'antropomorfismo) se lengthyComputation :: Int è ⊥ o n ot. Per fare ciò, deve valutare lengthyComputation :: Int.

---

Re aggiornamento:

newtype s sono unlifted, che significa che il costruttore non è un costruttore valore semanticamente (solo sintatticamente). La corrispondenza del motivo su un costruttore newtype è, a differenza della corrispondenza del modello su un costruttore data non rigido. Dato

newtype Foo a = Foo { unFoo :: a } -- record syntax for convenience below 

un "pattern match"

function :: Foo a -> Bar 
function (Foo x) = whatever x 

è del tutto equivalente a

function y = let x = unFoo y in whatever x 

La partita riesce sempre, e valuta nulla. The constructor only coerces the type e "corrispondenza modello" su di esso non vincola il tipo del valore.

seq è magico, non può essere implementato in Haskell. È possibile scrivere una funzione che corrisponde a seq per un tipo data, come il proprio seqMaybe sopra, in Haskell, ma non per un (polimorfico) newtype, perché "corrispondenza modello" sul costruttore newtype non è rigorosa. Dovresti corrispondere al/ai costruttore/i del tipo avvolto, ma per un polimorfico newtype, non li hai.