-- | Write functions in tacit (pointless) style using Applicative and De
-- Bruijn index notation.
--
-- Examples:
--
-- - @
-- \f x y -> f x == f y
-- = lurryA \@N3 ((==) \<$\> (_1 \<*\> _2) (_1 \<*\> _3))
-- @
-- - @
-- \f g x -> f x (g x)
-- = lurryA \@N3 ((_1 \<*\> _3) \<*\> (_2 \<*\> _3))
-- @
-- - @
-- \a b -> b
-- = lurryA \@N2 _2
-- @
--
-- This module is intended to be used with 'Control.Applicative' but
-- does not export it.
--
-- Opposite to De Bruijn indices, this module orders the arguments
-- from the outside-in, rather than the inside-out (or left-to-right
-- instead of right-to-left). For example, the conventional
-- @λλλ3 1 (2 1)@ is instead @λλλ1 3 (2 3)@.
--
-- The first argument is @z@, the second argument @z.s@, the third
-- argument @z.s.s@, and so on. For the first few arguments convenient
-- names have been defined, such as '_1', '_2', '_3', and so on.
--
-- To export a function use 'lurryA'. You must specify the arity of
-- the function, which is intended to be done with TypeApplications
-- (new in GHC 8.0). @lurryA \@(S Z) f@ says the arity of @f@ is one,
-- @lurryA \@(S (S Z)) f@ says the arity is two, and so on. For
-- convenience the first few Peano numbers have been given aliases,
-- such as @N1@, @N2@, @N3@, and so on.
--
-- You can write all functions with '<*>' and '<$>' from
-- 'Applicative' — should be able to, yet unproven.
--
-- There is a type inference problem with functions where the highest
-- index does not match the function arity, such as 'const'. To
-- resolve this ambiguity you must give an explicit signature. For
-- example: @lurryA \@N2 (_1 :: (a, (b, c)) -> a)@.
--
-- TODO:
--
-- - Construction rules for rewriting functions into this tacit form.
-- More precise than just examples. Would demonstrate that any
-- function can be written in this tacit form.
-- - An inverse for @lurry@, @unlurry@. Type inference seems
-- difficult.
-- - Inference problem when the highest index does not match the
-- function arity.
--
-- NOTES:
--
-- - The implementation would be simpler and less prone to inference
-- problems if GHC had closed classes. Given a type family @F@, a
-- corresponding value-level implementation may exist for
-- @x -> F x@. This implementation can be given by a class and an
-- instance corresponding to each case in the type family. However,
-- if the type family is closed and we only have open classes, we
-- cannot always define corresponding instances which are
-- unambiguous. An example of this correspondence is
-- 'Lurried'/'Lurry'.
--
{-# LANGUAGE
TypeFamilies
, FlexibleInstances
, FlexibleContexts
, DataKinds
, GADTs
, AllowAmbiguousTypes #-}
module Data.Function.Tacit
( Lurried
, Lurry(lurry)
, s, z
, _1, _2, _3, _4, _5, _6, _7, _8, _9
, Nat(Z, S)
, N0, N1, N2, N3, N4, N5, N6, N7, N8, N9
, Take
, lurryA
, shift
) where
import Prelude ((.), fst, snd)
-- | \"Curry\" a function type with a tuple-list argument.
--
-- Example:
--
-- @Lurried ((a, (b, (c, ()))) -> d) ~ a -> b -> c -> d@
--
type family Lurried (a :: *) where
Lurried ((a, () ) -> r) = a -> r
Lurried ((a, (b, cs)) -> r) = a -> Lurried ((b, cs) -> r)
--
-- | \"Curry\" a function with a tuple-list argument.
--
-- This type class should be treated as closed. The instances provided
-- map exactly to the type-level recursion defined by 'Lurried'.
--
-- Use 'lurryA' instead of 'lurry', which helps resolve ambiguity.
--
class Lurry f where
lurry :: f -> Lurried f
--
-- | Base case for 'Lurry'.
instance Lurry ((a, ()) -> r) where
lurry f = \a -> f (a, ())
--
-- | Recursive case for 'Lurry'.
instance (Lurry ((b, cs) -> r)) => Lurry ((a, (b, cs)) -> r) where
lurry f = \x -> lurry (\xs -> f (x, xs))
--
-- | First argument.
z :: (a, b) -> a
z = fst
-- | Next argument.
s :: (a, b) -> b
s = snd
-- | First argument.
_1 :: (a, b) -> a
_1 = z
-- | Second argument.
_2 :: (a, (b, c)) -> b
_2 = z.s
-- | Third argument.
_3 :: (a, (b, (c, d))) -> c
_3 = z.s.s
-- | Fourth argument.
_4 :: (a, (b, (c, (e, f)))) -> e
_4 = z.s.s.s
-- | Fifth argument.
_5 :: (a, (b, (c, (e, (f, g))))) -> f
_5 = z.s.s.s.s
-- | Sixth argument.
_6 :: (a, (b, (c, (e, (f, (g, h)))))) -> g
_6 = z.s.s.s.s.s
-- | Seventh argument.
_7 :: (a, (b, (c, (e, (f, (g, (h, i))))))) -> h
_7 = z.s.s.s.s.s.s
-- | Eighth argument.
_8 :: (a, (b, (c, (e, (f, (g, (h, (i, j)))))))) -> i
_8 = z.s.s.s.s.s.s.s
-- | Ninth argument.
_9 :: (a, (b, (c, (e, (f, (g, (h, (i, (j, k))))))))) -> j
_9 = z.s.s.s.s.s.s.s.s
-- | Cap a tuple-list to the given length.
--
-- Example:
--
-- @Take N2 (a, (b, (c, d))) ~ (a, (b, ()))@
--
type family Take (n :: Nat) (p :: *) where
Take (S Z) (a, _ ) = (a, ())
Take (S n) (a, (b, cs)) = (a, (Take n (b, cs)))
--
-- | Lurry a function of given arity. This arity must match exactly to
-- the highest index used to avoid ambiguity (see the module docs).
-- Otherwise, an explicit signature for the function must be given.
--
-- Example:
--
-- @lurryA \@N2 (_1 <*> _2) = ($)@
--
lurryA :: ( Take n p ~ p'
, p ~ p'
, Lurry (p -> r)
) =>
(p -> r) -> Lurried (p' -> r)
lurryA = lurry
-- | Peano numbers.
--
data Nat where
Z :: Nat
S :: Nat -> Nat
--
-- | The Peano number 0.
type N0 = Z
-- | The Peano number 1.
type N1 = S N0
-- | The Peano number 2.
type N2 = S N1
-- | The Peano number 3.
type N3 = S N2
-- | The Peano number 4.
type N4 = S N3
-- | The Peano number 5.
type N5 = S N4
-- | The Peano number 6.
type N6 = S N5
-- | The Peano number 7.
type N7 = S N6
-- | The Peano number 8.
type N8 = S N7
-- | The Peano number 9.
type N9 = S N8
-- | Increments the argument indices of a function.
--
-- Example:
--
-- @shift (_1 <*> _2) = _2 <*> _3@
--
shift :: ((b, c) -> d) -> (a, (b, c)) -> d
shift f (_, (b, c)) = f (b, c)