# Optimising newtype-like data types with existentials

## Motivation

Consider this data type declaration

data T where MkT :: !(Foo a) -> T

So `a`

is an existentially bound variable, and we cannot use a newtype for `T`

. So, as things stand, a value of type `T`

will be represented by a heap-allocated box containing a single pointer to a value of type `(Foo ty)`

for some `ty`

.

This is tantalising. The extra indirection and allocation gains nothing. Since `MkT`

is strict in its only argument, we could (at codegen time) *represent* a value of type `T`

by a value of type `Foo ty`

.

*This page does not propose any change whatsoever to the language*. Rather, it proposes
that we guarantee an efficient unboxed representation for certain data types.

The ticket to track this idea is #1965.

See also this OCaml pull request, which does exactly the same kind of thing for OCaml.

## Main design

Under what conditions can we guarantee to remove the box for a data type entirely?

- Only one constructor in the data type
- Only one field with nonzero width in that constructor (counting constraints as fields).
- That field is marked strict
- That field has a boxed (or polymorphic) type

Note that an equality constraint arising from a GADT has zero width, and thus is covered by (2). E.g.

data T a where MkT :: !Int -> T Int

The constructor actually has type

MkT :: forall a. (a ~# Int) => Int -> T a

So we could represent a value of type `(MkT a)`

by a plain `Int`

, without an indirection, because the evidence for `(a ~# Int)`

is zero width.

You might think that a single constructor GADT is probably not much use, but see Example 2 below.

## Some discussion

### Superclasses

David F: I believe condition 2 can be relaxed very slightly, to allow constraints known to be zero-width. For example, equality constraints should be fine. So should classes that have no methods and no superclasses with methods. For example, given

class This a ~ Int => Foo a class Foo a => Bar a where data BarType a class Bar a => Baz a where prox :: Proxy# a

David F: I *imagine* that `Foo a`

, `Bar a`

, and `Baz a`

contexts are zero-width.

SLPJ: no, class constraints are always boxed because they can be bottom (with recursive classes). I don't know how to avoid this.

David F: Does this mean even `~`

constraints are boxed? If so, that monkeys with GADT constructors that have equality constraints involving type families.

data Foo a b where Foo :: TF1 a ~ TF2 b => Foo a b

seems rather nicer than the alternative

data Foo a b where Foo :: !(TF1 a :~: TF2 b) -> Foo a b

Do such constraints just pile on extra junk?

### Strictness

Unlike a true `newtype`

, pattern matching on the constructor *must* force the contents to maintain type safety. In particular, matching on the constructor reveals an existential and/or type information. As Dan Doel found, and pumpkin relayed in https://ghc.haskell.org/trac/ghc/ticket/1965#comment:16, we have to be careful not to reveal such information without forcing the evidence. Since we're using the newtype optimization, the evidence is in the contained field itself.

*SLPJ: I do not understand this paragraph. Remember, we propose no change to the source language semantics*.

David F: I was simply clarifying that while this is the "newtype optimization", it is *not* about an actual `newtype`

. In both Haskell and Core it is `data`

, although Core could flag it as unusual if that's helpful.

## Sample uses

### Example 1

You might think that an existential data type with only one field is a bit unusual. Here is a example:

data Shape = Empty | NonEmpty data IntMap a = forall (e :: Shape) . IntMap !(IMGadt e a) data IMGadt (e :: Shape) a where Bin :: Prefix -> Mask -> IMGadt NonEmpty a -> IMGadt NonEmpty a -> IMGadt NonEmpty a Tip :: Key -> a -> IMGadt NonEmpty a Nil :: IMGadt Empty a

Here `IntMap`

obeys (1)-(4) and so `IntMap ty`

could be represented (without indirection) by the underlying `(IMGadt e ty)`

value, thereby saving an indirection at the root of every `IntMap`

.

A more direct rendering would look like this

data IntMap a = Empty | NonEmpty (NE a) data NE a = Bin Prefix Mask (NE a) (NE a) | Tip Key a

No GADTs, no existentials. But we get an indirection at the root of every non-empty `IntMap`

.

### Example 2

David Feuer: A single-constructor GADT can add a payload to something like

`Refl`

; it could also be used with a strict type-aligned sequence to "count", layering on length indexing. Admittedly not earth-shattering, but not totally useless.SLPJ: I still don't get it. Could you give an example?

For instance,

data TList c x y where Nil :: TList c x x Cons :: !(c x y) -> TList c y z -> TList c x z data Nat = Z | S Nat data LengthIncrement c p q where Inc :: !(c x y) -> LengthIncrement c '(S n, x) '(n, y)

Now `TList (LengthIncrement c) '(m, x) '(n, y)`

represents a type-aligned list taking a path from `x`

to `y`

, and having a length of `m - n`

. So while a single-constructor GADT may not be much use *on its own*, it can do something interesting when combined with another, multi-constructor GADT!

### Example 3

AntC: For anonymous records, you can wrap a payload in a newtype to label it within the record. But if you want to restrict (say) PersonId to being an Int, and yet have it look polymorphic, you have to make that a GADT. So now you're paying for the box.

For instance,

newtype Label1 a = Label1 a deriving (Eq, Read, Show) instance GetLabel (Label1 a) a where getLabel (Label1 x) = x {- can't do either of these: newtype PersonId = PersonId Int -- no type param newtype PersonId a = PersonId Int -- type param not used -} data PersonId a where PersonId :: !Int -> PersonId Int instance GetLabel (PersonId a) a where getLabel (PersonId x) = x -- using tuples as anon records: instance (a ~ a', GetLabel (l a) a') => HasField l (l a, lb, lc) a' where getField _ (x, _, _) = getLabel x

Of course there are many design choices for anon records and how to label their fields. (I'm trying not to pre-judge that.) But they'll all need that sort of type-indexed lookup -- including I think if the label is a type-level string.

Those GetLabel instances are tedious. When we have full-bore ORF, we can declare every data type using record syntax, all with field name unLabel.

data PersonId a where PersonId :: { unLabel :: !Int } -> PersonId Int ... getField _ (x, _, _) = unLabel x

### Layering evidence

data Foo a b c = Foo1 a b | Foo2 a b data Bar f a b c where Bar :: Family1 a b ~ True => !(f a b c) -> Bar a b c data Baz f a b c where Baz :: Family2 b c ~ True => !(f a b c) -> Baz a b c newtype Quux f a b c = Quux (Baz (Bar Foo) a b c)

With the newtype optimization, I can layer the `Baz`

type information on top of the `Bar`

type information on top of the `Foo`

type without having to pay a penalty. The alternative today is to make an entirely separate GADT for each combination of type information I want to hold evidence of.

## Implementation

Implementation is unfortunately tricky. Simply eliminating the boxing in Stg is easy, and this by itself saves us two words per value + pointer dereferencing. However, the generated code will be ugly, and if we could do this in Core instead of Stg, the simplifier would be able to do some follow-up optimizations and generate good code.

To be more specific, we want to do these transformations:

First:

D arg1 arg2 ... argN ==> nv_arg (where nv_arg is the only non-void argument)

(but we somehow need to bind other args or do substitution. If we do this Stg though we don't need to bind those args as unarise doesn't care about what a void argument is as long as it's void it gets rid of it and it can check void-ness by looking at Id's type)

Second:

case <exp1> of D arg1 arg2 ... argN -> <exp2> ==> let arg1 = ... arg2 = ... arg3 = ... in <exp2>

(we know only one of these args will be non-void, but all of them should be bound as they can be referred in <exp2>)

If we do this in Stg we lose some optimization opportunities and generate ugly code. For example, if the first transformation happens in a let-binding RHS maybe simplifier decides to inline it as it can't duplicate work after the transformation. Similarly it can decide to inline the non-void argument after second transformation which may lead to further optimizations etc.

For an example of an ugly code, suppose we had this:

case <exp1> of D (T x) -> <exp2>

in Stg this looks like

case <exp1> of D v -> case v of T x -> <exp2>

So now if we do the second transformation we get

let v = <exp1> in case v of T x -> <exp2>

but ideally we'd get

case <exp1> of T x -> <exp2>

Simplifier would be able to do this after the second transformation.

So the problem is

- If we implement this in Stg we generate ugly code, and miss some optimization opportunities (and arguably it doesn't buy us much, it saves 2 words per allocation + pointer dereferencing)

- Implementing this in Core is very hard, if not impossible, without losing type safety.

(copied from the mailing list discussion)