data-function-tacit (empty) → 0.1.0.0

raw patch · 4 files changed

+359/−0 lines, 4 filesdep +basesetup-changed

Dependencies added: base

Files

LICENSE +30/−0
Setup.hs +2/−0
data-function-tacit.cabal +32/−0
src/Data/Function/Tacit.hs +295/−0

+ LICENSE view

@@ -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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain

+ data-function-tacit.cabal view

@@ -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

+ src/Data/Function/Tacit.hs view

@@ -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)