Skip to content

CPR for constructors with existentials

Motivation

Consider the following two functions:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE UnboxedSums #-}

module Lib where

data Ex where
  Ex :: a -> Ex

data Box a where
  Box :: a -> Box a

f :: Int -> Ex
f n = case sum [1..n] of m -> Ex m
{-# NOINLINE f #-}

g :: Int -> Box Int
g n = case sum [1..n] of m -> Box m
{-# NOINLINE g #-}

If you look at the optimised Core, you'll see that g was worker/wrappered to expose the Box constructor, while f was not. consequently, call sites can't cancel away the Ex constructor. I don't see why we can't do this transformation, with a little help from unboxed sums in the general case (although we probably want CPR for sums first, which in turn depends on Nested CPR...).

Proposal

Make CPR recognise non-vanilla constructed products (let's focus on existentials in this ticket): Group construction sites by how they instantiate existential type parameters. Each of these groups becomes an alternative in the unboxed sum constructed by WW. Example

{-# LANGUAGE GADTs #-}
{-# LANGUAGE UnboxedSums #-}
{-# LANGUAGE TypeApplications #-}

module Lib where

data Ex where
  Ex :: a -> Ex

f :: Int -> Ex
f n = case sum [1..n] of
  0 -> Ex @Bool True
  1 -> Ex @Char 'a'
  2 -> Ex @Char 'b'
  m -> Ex @Int m
{-# NOINLINE f #-}

fwork :: Int -> (# Bool | Char | Int #)
fwork n = case sum [1..n] of
  0 -> (# True |     |   #)
  1 -> (#      | 'a' |   #)
  2 -> (#      | 'b' |   #)
  m -> (#      |     | m #)

fwrap :: Int -> Ex
fwrap n = fwork n of
  (# b |   |   #) -> Ex b
  (#   | c |   #) -> Ex c
  (#   |   | m #) -> Ex m

Where fwrap is the wrapper of f after optimisations. Note how there are only 3 alternatives in the sum because Ex was instantiated at Char twice.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information