Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is the WHNF of a newtype and how does rseq work on a newtype?

Since newtypes are effectively removed during compilation, they don't have thunks, just values. So what happens if I ask for its WHNF using rseq? For example in

Sum (lengthyComputation :: Int) `using` rseq

where Sum is defined as

newtype Sum a = Sum { getSum :: a }

will lengthyComputation get evaluated or not? Is it specified/documented somewhere so that I can count on it?


Update: Let me explain my doubts in more detail. Intuitively one says: "newtype is strict so clearly its WHNF is the WHNF of what's wrapped inside". But I feel this is a very imprecise shortcut and the reasoning is not so clear. Let me give an example:

For standard data types, WHNF can defined as a form where we know which constructor was used for constructing the value. If, for example, we didn't have seq, we could create our own

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

and similarly for any data type, just by pattern matching on one of its constructors.

Now let's take

newtype Identity a = Identity { runIdentity :: a }

and create a similar seqIdentity function:

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

clearly, nothing is forced to WHNF here. (After all, we always know what constructor was used.) After compilation, seqIdentity will be identical to const id. In fact, it isn't possible to create polymorphic seqIdentity such that it would force evaluation of a value wrapped inside Identity! We could define WHNF a of a newtype to be simply the value unmodified, and it would be consistent. So I believe the question is, how is WHNF defined for newtypes? Or is there no rigorous definition, and the behavior "it's the WHNF of what's inside" is simply assumed as something obvious?

like image 419
Petr Avatar asked Dec 02 '12 12:12

Petr


1 Answers

Per the section on Datatype renamings in the report,

Unlike algebraic datatypes, the newtype constructor N is unlifted, so that N ⊥ is the same as ⊥.

Here

Sum ⊥ = ⊥

so the weak head normal form of a newtype is the WHNF of the wrapped type, and

Sum (lengthyComputation :: Int) `using` rseq

evaluates lengthyComputation (when the entire expression is evaluated, a mere binding

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

of course doesn't, but that is the same without the newtype constructor).

The defining equations for seq are

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

and hence

seq (Sum ⊥) b = ⊥

and in

seq (lengthyComputaton :: Int) b

the seq is required to find out (sorry for the anthropomorphism) whether lengthyComputation :: Int is ⊥ or not. To do that, it must evaluate lengthyComputation :: Int.


Re update:

newtypes are unlifted, that means that the constructor is not a value constructor semantically (only syntactically). Pattern-matching on a newtype constructor is, in contrast to pattern matching on a data constructor not strict. Given

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

a "pattern match"

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

is completely equivalent to

function y = let x = unFoo y in whatever x

The match always succeeds, and evaluates nothing. The constructor only coerces the type and "pattern matching" on it un-coerces the type of the value.

seq is magic, it cannot be implemented in Haskell. You can write a function that does the same as seq for a data type, like your seqMaybe above, in Haskell, but not for a (polymorphic) newtype, because "pattern matching" on the newtype constructor is not strict. You would have to match on the constructor(s) of the wrapped type, but for a polymorphic newtype, you don't have them.

like image 113
Daniel Fischer Avatar answered Nov 07 '22 05:11

Daniel Fischer