summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorerisco <>2016-06-01 00:16:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2016-06-01 00:16:00 (GMT)
commit69e166f40e9ee6d42f1b5e3af91142cab033fdd5 (patch)
tree9caba8642546a2420ef8cb175b52861bbc7dbd31
version 0.1.0.0HEAD0.1.0.0master
-rw-r--r--LICENSE30
-rw-r--r--Setup.hs2
-rw-r--r--data-function-tacit.cabal32
-rw-r--r--src/Data/Function/Tacit.hs295
4 files changed, 359 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..58daf91
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2016, Eric Brisco (eric.brisco@gmail.com)
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of Eric Brisco nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..833b4c6
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/data-function-tacit.cabal b/data-function-tacit.cabal
new file mode 100644
index 0000000..81c0f3c
--- /dev/null
+++ b/data-function-tacit.cabal
@@ -0,0 +1,32 @@
+name: data-function-tacit
+version: 0.1.0.0
+synopsis: Write functions in tacit (pointless) style using Applicative and De Bruijn index notation.
+description: Write functions in tacit (pointless) style using Applicative and De Bruijn index notation.
+homepage: https://github.com/erisco/data-function-tacit
+license: BSD3
+license-file: LICENSE
+author: Eric Brisco
+maintainer: eric.brisco@gmail.com
+copyright: Copyright (c) 2016, Eric Brisco
+category: Data
+build-type: Simple
+cabal-version: >=1.10
+
+library
+
+ exposed-modules: Data.Function.Tacit
+
+ build-depends: base >=4.6 && <5
+
+ hs-source-dirs: src
+
+ default-language: Haskell2010
+
+source-repository head
+ type: git
+ location: https://github.com/erisco/data-function-tacit
+
+source-repository this
+ type: git
+ location: https://github.com/erisco/data-function-tacit
+ tag: v0.1.0.0
diff --git a/src/Data/Function/Tacit.hs b/src/Data/Function/Tacit.hs
new file mode 100644
index 0000000..4565ef2
--- /dev/null
+++ b/src/Data/Function/Tacit.hs
@@ -0,0 +1,295 @@
+-- | 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)