Test.StrictCheck.Curry

This module defines a flexible and efficient way to curry and uncurry functions of any arity. This is useful in the context of StrictCheck to provide a lightweight interface to test developers which does not require them to directly work with heterogeneous lists.

Computing the types of curried functions

type family (args :: [*]) ⋯-> (rest :: *) :: * where ...

Given a list of argument types and the "rest" of a function type, return a curried function type which takes the specified argument types in order, before returning the given rest

For example:

[Int, Bool] ⋯-> Char  ~  Int -> Bool -> Char

This infix unicode symbol is meant to evoke a function arrow with an ellipsis.

Equations

'[] ⋯-> rest = rest

(a ': args) ⋯-> rest = a -> args ⋯-> rest

type (-..->) args rest = args ⋯-> rest

For those who don't want to type in unicode, we provide this ASCII synonym for the ellipsis function arrow (⋯->)

type family Args (f :: *) :: [*] where ...

Given a function type, return a list of all its argument types

For example:

Args (Int -> Bool -> Char)  ~  [Int, Bool]

Equations

Args (a -> rest) = a ': Args rest

Args x = '[]

type family Result (f :: *) :: * where ...

Strip all arguments from a function type, yielding its (non-function-type) result

For example:

Result (Int -> Bool -> Char)  ~  Char

Equations

Result (a -> rest) = Result rest

Result r = r

Currying functions at all arities

class Curry (args :: [*]) where

The Curry class witnesses that for any list of arguments, it is always possible to curry/uncurry at that arity

Minimal complete definition

uncurry, curry

Methods

uncurry :: forall result list. List list => (args ⋯-> result) -> list args -> result

curry :: forall result list. List list => (list args -> result) -> args ⋯-> result

Instances

Curry ([] *)

Methods

uncurry :: List list => ([*] ⋯-> result) -> list [*] -> result

curry :: List list => (list [*] -> result) -> [*] ⋯-> result

Curry xs => Curry ((:) * x xs)

Methods

uncurry :: List list => ((* ': x) xs ⋯-> result) -> list ((* ': x) xs) -> result

curry :: List list => (list ((* ': x) xs) -> result) -> (* ': x) xs ⋯-> result

curryAll :: forall args result list. (List list, Curry args) => (list args -> result) -> args ⋯-> result

Curry all arguments to a function from a heterogeneous list to a result

This is a special case of curry, and may ease type inference.

uncurryAll :: forall function list. (List list, Curry (Args function)) => function -> list (Args function) -> Result function

Uncurry all arguments to a function type

This is a special case of uncurry, and may ease type inference.

withCurryIdentity :: forall function r. (function ~ (Args function ⋯-> Result function) => r) -> r

For any function type function, it is always true that

function  ~  (Args function ⋯-> Result function)

GHC doesn't know this, however, so withCurryIdentity provides this proof to the enclosed computation, by discharging this wanted equality constraint.

Generalized to any heterogeneous list

class List (list :: [*] -> *) where

This currying mechanism is agnostic to the concrete heterogeneous list type used to carry arguments. The List class abstracts over the nil and cons operations of a heterogeneous list: to use your own, just define an instance.

Minimal complete definition

nil, cons, uncons

Methods

nil :: list '[]

cons :: x -> list xs -> list (x ': xs)

uncons :: list (x ': xs) -> (x, list xs)

Instances

List (NP * I)

Methods

nil :: NP * I [*]

cons :: x -> NP * I xs -> NP * I ((* ': x) xs)

uncons :: NP * I ((* ': x) xs) -> (x, NP * I xs)