packages feed

defun (empty) → 0.1

raw patch · 5 files changed

+360/−0 lines, 5 filesdep +basedep +defundep +defun-bool

Dependencies added: base, defun, defun-bool, defun-core, defun-sop, sop-core

Files

+ CHANGELOG.md view
@@ -0,0 +1,3 @@+## 0.1++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2023, Oleg Grenrus++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 Oleg Grenrus 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.
+ defun.cabal view
@@ -0,0 +1,85 @@+cabal-version:   2.4+name:            defun+version:         0.1+license:         BSD-3-Clause+license-file:    LICENSE+author:          Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer:      Oleg Grenrus <oleg.grenrus@iki.fi>+category:        Data+build-type:      Simple+extra-doc-files: CHANGELOG.md+tested-with:     GHC ==9.2.8 || ==9.4.8 || ==9.6.3 || ==9.8.1+synopsis:        Defunctionalization helpers+description:+  The package @defun@ provides defunctionalization helpers, most importantly+  type family 'DeFun.Core.App' allowing to write higher-order type families.+  The @singletons@ package also has its own type family @Apply@,+  but the machinery is tied to the @Sing@ / singletons.+  .+  Once @UnsaturatedTypeFamilies@ extension is implemented in GHC+  ([Proposal 242](https://github.com/ghc-proposals/ghc-proposals/pull/242)),+  this package will become more or less obsolete.+  .+  In particular, the @Lam@ counterpart @SLambda@ is specialized to @Sing@ arguments.+  The @defun@'s @Lam@ is however fully general, so you can use your own singletons+  or (importantly) singleton-like arguments.+  .+  The package provides few defunctionalized functions, and their term-level+  reflections using @SBool@ and @NP@ data types from @singletons-bool@ and @sop-core@+  packages respectively.+  .+  This is the "batteries-included" variant with "many" dependencies; see the+  @defun-core@ package and other @defun-*@ dependencies if you need a more limited+  dependency footprint.+  .+  The [first-class-families](https://hackage.haskell.org/package/first-class-families) package has slightly different design,+  in particular it doesn't reuse existing (nor define) own standalone type families.+  In @first-class-families@ everything has to be evaluated via its @Eval@ type family (which job is similar to @App@),+  but @defun@ only makes /higher-order/ type families look different.+  In short, ergonomics are a bit different.++source-repository head+  type:     git+  location: https://github.com/phadej/defun.git+  subdir:   defun++common language+  default-language:   Haskell2010+  default-extensions:+    DataKinds+    EmptyCase+    GADTs+    KindSignatures+    NoImplicitPrelude+    PatternSynonyms+    PolyKinds+    RankNTypes+    ScopedTypeVariables+    StandaloneKindSignatures+    TypeApplications+    TypeFamilies+    TypeOperators+    UndecidableInstances+    ViewPatterns++library+  import:                   language+  hs-source-dirs:           src+  exposed-modules:          DeFun+  build-depends:+    , defun-bool  >=0.1 && <0.1.1+    , defun-core  >=0.1 && <0.1.1+    , defun-sop   >=0.1 && <0.1.1++  x-docspec-extra-packages: base+  x-docspec-options:        -XDataKinds -XGADTs -XStandaloneDeriving++test-suite defun-tests+  import:         language+  type:           exitcode-stdio-1.0+  hs-source-dirs: test+  main-is:        defun-tests.hs+  build-depends:+    , base <5+    , defun+    , sop-core
+ src/DeFun.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE Trustworthy #-}+module DeFun (+    -- * Introduction+    -- $intro+    --++    -- * Implementation+    module DeFun.Core,+    module DeFun.Function,+    module DeFun.Bool,+    module DeFun.List,+    module Data.SOP.NP.DeFun,+    module SBool.DeFun,+) where++import Data.SOP.NP.DeFun+import DeFun.Bool+import DeFun.Core+import DeFun.Function+import DeFun.List+import SBool.DeFun++-- $intro+--+-- This package provides defunctionalization helpers to write+-- type-level computations.+--+-- As [UnsaturatedTypeFamilies](https://github.com/ghc-proposals/ghc-proposals/pull/242) are not yet implemented in the GHC,+-- we cannot define type-level type families.+-- Or we can, but we could only apply them to type-constructors:+--+-- @+-- type BadMap :: (a -> b) -> [a] -> [b]+-- type family BadMap f xs where+--     BadMap f '[]      = '[]+--     BadMap f (x : xs) = f x : BadMap f xs+-- @+--+-- can be only applied to type or data-constructors,+-- i.e. @BadMap Just [1, 2, 3]@ would work, but @BadMap 'Not' [True, False]@+-- will not.+--+-- The trick is to defunctionalize higher-order functions. Instead of taking+-- a function argument, we'll take a defunctionalization /symbol/,+-- and use 'App' type family to apply it:+--+-- @+-- type Map :: (a ~> b) -> [a] -> [b]+-- type family Map f xs where+--     Map f '[]    = '[]+--     Map f (x:xs) = f @@ x : Map f xs+-- @+--+-- where '@@' is the application operator.+--+-- Now we can call @'Map' 'NotSym' [True, False]@ and it will compute.+-- The @'Map' Just [1, 2, 3]@ wont work, we need to convert a constuctor+-- into a symbol @'Map' (Con1 Just) [1, 2, 3]@ works.+--+-- Then, the @Map@ itself can be defunctionalized.+-- We need to define two symbols, as @Map@ takes two arguments:+--+-- @+-- type MapSym :: (a ~> b) ~> [a] ~> [b]+-- data MapSym f+-- type instance App MapSym f = MapSym1 f+--+-- type MapSym1  :: (a ~> b) -> [a] ~> [b]+-- data MapSym1 f xs+-- type instance App (MapSym1 f) xs = Map f xs+-- @+--+-- So far the above is general enough, and is defined in @singletons@+-- (sans using different names) in a similar way.+--+-- Another thing which we also need, is to represent the type-level computation at type level as well.+-- The @singletons@ package uses @Sing@ type-family, that's the whole package of that package.+--+-- However, @Sing@ is quite resticting. For example, one natural "term-level" reflection of lists+-- is 'Data.SOP.NP.NP' type.+--+-- For example given 'Append' type family, we can write a very useful 'append' function:+--+-- @+-- append :: NP a xs -> NP a ys -> NP a (Append xs ys)+-- append Nil       ys = ys+-- append (x :* xs) ys = x :* append xs ys+-- @+--+-- @singletons@ machinery doesn't help us define these.+--+-- Then 'Append' (and 'append') can be used as an argument (to e.g. 'Map') and 'map':+-- we can write something like+--+-- @+-- mapAppend xs yss = map (appendSym @@ xs) yss+-- @+--+-- and GHC will infer the type+--+-- @+-- mapAppend :: NP a xs -> NP (NP a) xss -> NP (NP a) (Map (AppendSym1 xs) xss)+-- @+--+-- to that function.+--+-- Being able to relatively easily write functions like 'mapAppend'+-- is the main motivation for creation of @defun@ package.+--+-- Another example is append to n-ary sums ('NS'):+--+-- @+-- append_NS :: forall xs ys f sing. NP sing xs -> Either (NS f xs) (NS f ys) -> NS f (Append xs ys)+-- append_NS _ (Left xs) = goLeft xs where+--     goLeft :: NS f xs' -> NS f (Append xs' ys)+--     goLeft (Z x) = Z x+--     goLeft (S x) = S (goLeft x)+-- append_NS xs (Right ys0) = goRight xs ys0 where+--     goRight :: NP sing xs' -> NS f ys -> NS f (Append xs' ys)+--     goRight Nil       ys = ys+--     goRight (_ :* xs) ys = S (goRight xs ys)+-- @+--+-- where we use @NP sing@ as an explicit singleton for @xs@,+-- instead of using @SingI@ from @singletons@ or @All@ from @sop-core@.+--+-- In my experience, using explicit "singletons" (especially in a libraries' internal plumbing)+-- is a lot more convenient than trying to create all required @All@ dictionaries+-- (then you would need to write everything twice, 'Type' and 'Constraint' versions: i.e. for 'NP' and 'All', or convert back and forth between @NP (Dict c)@ and @All c@).+--
+ test/defun-tests.hs view
@@ -0,0 +1,112 @@+module Main where++import Data.SOP (NP (..), NS (..))+import GHC.Generics ((:*:) (..))+import Prelude (IO, putStrLn, Either (..))++import qualified Prelude as P++import DeFun++main :: IO ()+main = putStrLn "OK"++-------------------------------------------------------------------------------+-- mapAppend+-------------------------------------------------------------------------------++mapAppend :: NP a xs -> NP (NP a) xss -> NP (NP a) (Map (AppendSym1 xs) xss)+mapAppend xs yss = map (appendSym @@ xs) yss++-------------------------------------------------------------------------------+-- split_NP+-------------------------------------------------------------------------------++-- | inverse of 'append'+split_NP :: NP pa xs -> NP a (Append xs ys) -> (NP a xs, NP a ys)+split_NP Nil       xys        = (Nil, xys)+split_NP (_ :* ps) (x :* xys) = let (xs, ys) = split_NP ps xys in (x :* xs, ys)++-------------------------------------------------------------------------------+-- FLATTEN utils+-------------------------------------------------------------------------------++map_NS :: Lam a b f -> NS a xs -> NS b (Map f xs)+map_NS f (Z x)  = Z (f @@ x)+map_NS f (S xs) = S (map_NS f xs)++map_NS' :: Lam (px :*: a) b f -> NP px xs -> NS a xs -> NS b (Map f xs)+map_NS' _ Nil         x      = case x of {}+map_NS' f (px :* _)   (Z x)  = Z (f @@ (px :*: x))+map_NS' f (_  :* pxs) (S xs) = S (map_NS' f pxs xs)++append_NS :: forall xs ys f sing. NP sing xs -> Either (NS f xs) (NS f ys) -> NS f (Append xs ys)+append_NS _ (Left xs) = goLeft xs where+    goLeft :: NS f xs' -> NS f (Append xs' ys)+    goLeft (Z x) = Z x+    goLeft (S x) = S (goLeft x)+append_NS xs (Right ys0) = goRight xs ys0 where+    goRight :: NP sing xs' -> NS f ys -> NS f (Append xs' ys)+    goRight Nil        ys = ys+    goRight (_ :* xs') ys = S (goRight xs' ys)++concatMap_NS :: Lam pa (NP pb) f -> NP pa xs -> Lam a (NS b) f -> NS a xs -> NS b (ConcatMap f xs)+concatMap_NS pf pxs f = concatMap_NS' pf pxs (Lam (\(_ :*: x) -> f @@ x))++concatMap_NS' :: Lam pa (NP pb) f -> NP pa xs -> Lam (pa :*: a) (NS b) f -> NS a xs -> NS b (ConcatMap f xs)+concatMap_NS' _  Nil         = \_ xs -> case xs of {}+concatMap_NS' pf (px :* pxs) = concatMap_NS_aux' pf px pxs++concatMap_NS_aux' :: forall a b f x xs pa pb. Lam pa (NP pb) f -> pa x -> NP pa xs -> Lam (pa :*: a) (NS b) f -> NS a (x : xs) -> NS b (ConcatMap f (x : xs))+concatMap_NS_aux' pf px _pxs f (Z x) = append_NS+    @_+    @(ConcatMap f xs)+    (pf @@ px)+    (Left (f @@ (px :*: x)))+concatMap_NS_aux' pf px pxs f (S xs) = append_NS+    @_+    @(ConcatMap f xs)+    (pf @@ px)+    (Right (concatMap_NS' pf pxs f xs))++map2_NS :: forall a b c f xs ys pa pb pc.+    Lam2 pa pb pc f -> NP pa xs -> NP pb ys ->+    Lam2 a b c f -> NS a xs -> NS b ys -> NS c (Map2 f xs ys)+map2_NS pf pxs pys f xs ys = concatMap_NS+    (compSym2 (flipSym2 mapSym pys) pf)+    pxs+    (compSym2 (flipSym2 (mkLam2 map_NS) ys) f)+    xs++sequence_NSNP :: NP (NP sing) xss -> NP (NS f) xss -> NS (NP f) (Sequence xss)+sequence_NSNP Nil         Nil         = Z Nil+sequence_NSNP (xs :* xss) (ys :* yss) = map2_NS+    (con2 (:*))+    xs+    (sequence xss)+    (con2 (:*))+    ys+    (sequence_NSNP xss yss)++sequence_NSNP_sym :: Lam (NP (NP sing) :*: NP (NS f)) (NS (NP f)) SequenceSym+sequence_NSNP_sym = Lam (\(pxss :*: xss) -> sequence_NSNP pxss xss)++-------------------------------------------------------------------------------+-- FLATTEN+-------------------------------------------------------------------------------++-- given as sum-of-products of sum-of-products,+-- we can turn it into big sum-of-products.++flattenList :: [[[[k]]]] -> [[k]]+flattenList = P.concatMap (P.map P.concat P.. P.sequence)++type FLATTEN xsss = ConcatMap (CompSym2 (MapSym1 ConcatSym) SequenceSym) xsss++-- This is an isomorphism.+flatten_NSNP :: forall xssss f sing. NP (NP (NP (NP sing))) xssss -> NS (NP (NS (NP f))) xssss -> NS (NP f) (FLATTEN xssss)+flatten_NSNP pxssss xssss = concatMap_NS'+    (compSym2 (mapSym1 concatSym) sequenceSym)+    pxssss+    (compSym2 (Lam (map_NS concatSym)) sequence_NSNP_sym)+    xssss