Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.ExpandCase

Description

This module is intended for high-performance programming. Concretely, the ExpandCase class can be used to force GHC to avoid compiling Reader, Endo or State-based code to unnecessary closures. You can observe its usage in Generic. For a smaller example and some explanation, consider the following.

f :: Bool -> Endo Int
f b = case b of
  True  -> mempty
  False -> Endo (+ 10)

The desired -O1 output should be the following (ignoring newtype casts):

f = b n -> case b of
  True  -> n
  False -> n + 10

A typical undesired output would be

f = b -> case b of
  True  -> n -> n
  False -> n -> n + 10

Returning closures can be better or worse, depending on the program context. However, in high-performance situations we almost never want to return closures, and GHC is not nearly reliable enough at getting rid of the closures.

Using ExpandCase, we can write code as follows.

f :: Bool -> Endo Int
f b = expand ret -> case b of
  True  -> ret mempty
  False -> ret $ Endo (+10)

Here, expand immediately introduces a lambda abstraction, and the ret continuation applies the "body" of the definition to the freshly abstracted variable. Hence, we get something like the following as an intermediate piece of Core:

f :: Bool -> Endo Int
f b = Endo n -> case b of
  True  -> appEndo mempty n
  False -> appEndo (Endo (+10)) n

which is then reliably optimized to

f :: Bool -> Endo Int
f b = Endo n -> case b of
  True  -> n
  False -> n + 10

NOTE: if you want to use this module, it is very strongly recommended that you check the Core of your code!

Documentation

class ExpandCase a where Source #

Minimal complete definition

Nothing

Associated Types

type Result a Source #

Methods

expand :: ((a -> Result a) -> Result a) -> a Source #

default expand :: Result a ~ a => ((a -> Result a) -> Result a) -> a Source #

Instances

Instances details
ExpandCase All Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result All 
Instance details

Defined in Agda.Utils.ExpandCase

type Result All = All

Methods

expand :: ((All -> Result All) -> Result All) -> All Source #

ExpandCase Any Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result Any 
Instance details

Defined in Agda.Utils.ExpandCase

type Result Any = Any

Methods

expand :: ((Any -> Result Any) -> Result Any) -> Any Source #

ExpandCase () Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result () 
Instance details

Defined in Agda.Utils.ExpandCase

type Result () = ()

Methods

expand :: ((() -> Result ()) -> Result ()) -> () Source #

ExpandCase Bool Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result Bool 
Instance details

Defined in Agda.Utils.ExpandCase

Methods

expand :: ((Bool -> Result Bool) -> Result Bool) -> Bool Source #

ExpandCase Int Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result Int 
Instance details

Defined in Agda.Utils.ExpandCase

type Result Int = Int

Methods

expand :: ((Int -> Result Int) -> Result Int) -> Int Source #

ExpandCase (Endo a) Source # 
Instance details

Defined in Agda.Utils.StrictEndo

Associated Types

type Result (Endo a) 
Instance details

Defined in Agda.Utils.StrictEndo

type Result (Endo a) = a

Methods

expand :: ((Endo a -> Result (Endo a)) -> Result (Endo a)) -> Endo a Source #

ExpandCase (Endo a) Source # 
Instance details

Defined in Agda.Utils.StrictFlipEndo

Associated Types

type Result (Endo a) 
Instance details

Defined in Agda.Utils.StrictFlipEndo

type Result (Endo a) = a

Methods

expand :: ((Endo a -> Result (Endo a)) -> Result (Endo a)) -> Endo a Source #

ExpandCase (Endo a) Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result (Endo a) 
Instance details

Defined in Agda.Utils.ExpandCase

type Result (Endo a) = a

Methods

expand :: ((Endo a -> Result (Endo a)) -> Result (Endo a)) -> Endo a Source #

ExpandCase (IO a) Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result (IO a) 
Instance details

Defined in Agda.Utils.ExpandCase

type Result (IO a) = IO a

Methods

expand :: ((IO a -> Result (IO a)) -> Result (IO a)) -> IO a Source #

ExpandCase (Maybe a) Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result (Maybe a) 
Instance details

Defined in Agda.Utils.ExpandCase

type Result (Maybe a) = Maybe a

Methods

expand :: ((Maybe a -> Result (Maybe a)) -> Result (Maybe a)) -> Maybe a Source #

ExpandCase [a] Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result [a] 
Instance details

Defined in Agda.Utils.ExpandCase

type Result [a] = [a]

Methods

expand :: (([a] -> Result [a]) -> Result [a]) -> [a] Source #

ExpandCase a => ExpandCase (Reader r a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Associated Types

type Result (Reader r a) 
Instance details

Defined in Agda.Utils.StrictReader

type Result (Reader r a) = Result a

Methods

expand :: ((Reader r a -> Result (Reader r a)) -> Result (Reader r a)) -> Reader r a Source #

ExpandCase (Pair a b) Source # 
Instance details

Defined in Agda.Utils.ExpandCase

Associated Types

type Result (Pair a b) 
Instance details

Defined in Agda.Utils.ExpandCase

type Result (Pair a b) = Pair a b

Methods

expand :: ((Pair a b -> Result (Pair a b)) -> Result (Pair a b)) -> Pair a b Source #

ExpandCase (m a) => ExpandCase (ReaderT r m a) Source # 
Instance details

Defined in Agda.Utils.StrictReader

Associated Types

type Result (ReaderT r m a) 
Instance details

Defined in Agda.Utils.StrictReader

type Result (ReaderT r m a) = Result (m a)

Methods

expand :: ((ReaderT r m a -> Result (ReaderT r m a)) -> Result (ReaderT r m a)) -> ReaderT r m a Source #

ExpandCase (m (Pair a s)) => ExpandCase (StateT s m a) Source # 
Instance details

Defined in Agda.Utils.StrictState

Associated Types

type Result (StateT s m a) 
Instance details

Defined in Agda.Utils.StrictState

type Result (StateT s m a) = Result (m (Pair a s))

Methods

expand :: ((StateT s m a -> Result (StateT s m a)) -> Result (StateT s m a)) -> StateT s m a Source #