The runXXXX element in a newtype definition

Learn
1

In the writer monad definition, we have

newtype Writer w a = Writer { runWriter :: (a,w) }

instance (Monoid w) => Monad (Writer w) where
  return a = Writer (a,mempty)
  (Writer (a,w)) >>= f = let (a',w') = runWriter $ f a in Writer (a',w `mappend` w')

I come from the ML/Isabelle world, where we have one name for a datatype, what is Writer here. This could be written as

datatype ('a, 'w) writerMonad = Writer ('a * 'w)

and in a function definition, I could write a pattern as

"myFunction (Writer (a,w)) = ..."

But what is runWriter in that scenario? What does it do?

2

It is just a field name in a record notation.

1 Like
3

the newtype declaration results in this definition:

runWriter :: Writer w a -> (a, w)
runWriter (Writer x) = x
1 Like
4

So it unpacks the content of the type, as I understand?

2 Likes
5

Yup, accessor functions are just a handy way not to always have to pattern match data.

6

But note that you can have multiple selectors which unpacks different part of a type:

data Person = Person { name :: String, age :: Int }

Now name :: Person -> String selects the name of the person and age :: Person -> Int selects the age of the person.

2 Likes
7

As a side note, I really don’t like naming (newtype) field selectors runXXX:

  1. It’s confusing if you’re not used to it (although that’s quite a subjective argument)
  2. The pattern is coincidental; runXXX refers to running/unpacking an effect (I think) and by sheer coincidence that’s the only field of Writer m. Better use a common field name such as unXXX (commn for newtypes) or something like writerAction and use that to define an exported runWriter function
  3. Case in point: If you export runXXX, you implicitly export “the innards” of your newtype. Depending on your definition, this means you also export the ability to coerce away the newtype constructor. Not so if you have a separate function runWriter with a field selector writerAction that is not exported. I was wrong about this, see below. But the same applies to record update syntax, which doesn’t make sense considering the name runWriter.

Although in practice, I suppose this hardly worth splitting hairs over…

2 Likes
9

I think the convention is perfectly fine. It’s confusing when you’re not quite used to the idea record accessors are “just functions”, and thinking of them as such, but this idea is essential to writing idiomatic Haskell. Just look at GADT syntax, which highlights this even more:

data Writer w a where
    runWriter :: Writer w a -> (a, w)

Using this notation, we are conceptually no longer saying "Writer is a data type, parametrized over two types w and a, that has one field called runWriter, whose type is (a, w)"; we are saying "there exists a type Writer, parametrized over two types w and a, for which a function runWriter exists, whose type is Writer w a -> (a, w)". It’s literally the same thing, the difference is purely in the surface syntax, but the viewpoint is a different one.

This idea of data types and functions being the same thing, or at least isomorphic, permeates Haskell, and many common idioms can only be fully understood if you have developed an intuition for this. Is a list a data structure or a control construct? Yes! Is Functor an abstraction of data structures or control flow? Also yes! What’s up with the Data vs. Control namespaces? Nothing but historical cruft, really! Or look at DLists, which literally represent lists as functions. Or defunctionalization as a programming technique.

So while writing runWriter as a “field” may be confusing to a beginner, that confusion cannot be avoided entirely, and IMO that makes it a weak argument against using it here.

10

That GADT syntax is not correct. The correct syntax is:

data Writer w a where
    Writer :: { runWriter :: (a, w) } -> Writer w a

Maybe you’re confusing GADT syntax with Agda’s codata syntax? I think that would be more like what you wrote.

Actually, it would be pretty interesting to introduce codata syntax in Haskell. It might make definitions like this easier to read.

1 Like
11

Case in point: If you export runXXX, you implicitly export “the innards” of your newtype. Depending on your definition, this means you also export the ability to coerce away the newtype constructor.

I don’t think this is true: you can export runWriter without exporting the constructor.

12

Wha? where is that syntax valid? It’s not a GADT declaration that I recognise. Neither does GHC.

Comes from lambda calculus, and is therefore in LISP, because neither of those have any concept of data constructors or pattern matching.

Not my thinking in Haskell it doesn’t.

This fails to explain where a value of type Writer w a ‘comes from’. And that’s why it’s so puzzling for newbies. Much easier to think that applying a data constructor builds a value with components; pattern matching takes apart those components. So GADT syntax – even when it’s legit GADT syntax – fails to show that.

(Yes there’s a convoluted story such that we can in lambda calculus build something isomorphic to a data constructor that is higher-order and takes an extra parameter that’s an extractor function. Isomorphic does not mean " literally the same thing, the difference is purely in the surface syntax,". You’re telling fairy-stories.)

1 Like
13

Right, good point. Nevertheless, I think exporting a field selector that by coincidence is the implementation of the eliminator of an effect and hence naming it as such seems smart on first blush, but is just confusing the more you think about it. For example

f :: Writer w a -> Writer [Int] ()
f w = w { runWriter = ((), []) }

is not something that makes sense for the user to write…

3 Likes
14

Only in crazy Haskell (98) with a field name restricted to a single data type would that idea occur to anyone. Leaving aside the status of data constructors, if Haskell had records like nearly every other modern programming language [**], you’d have to think of record accessors as overloaded for every data type in which a field with that name might appear – and potentially at a different resulting field type.

[**] And I don’t think this has anything to do with functional vs procedural/OO; or with strict vs lazy.

1 Like
16

Ah, apologies: all this sidetracking into GADT syntax and components has missed your question. Writer is a newtype. (Not a data, as others and including me have started talking about.)

newtypes must have a single ‘component’; and because of that, the data constructor Writer isn’t really a constructor/wrapper; and the field name runWriter isn’t really an ‘extractor’.

What we really have is a pair type (a,w) – yes same as ('a * 'w) – with a (not-very) magic cloak that stops it getting taken as a pair, and enables it to enter into the (very definitely) magic world of Monads.

runWriter slips off the cloak, once we step into the magic world.

17

Agreed, the problem is update syntax. It give the means to violate internal invariants:

newtype NonZero = UnsafeNonZero { unNonzero :: Int }

...

bad :: NonZero -> NonZero
bad x = x { unNonZero = 0 }

I have made this mistake myself. It took some time before I noticed what I had done…

18

Gah, what an incredible brainfart…