**diff options**

author | aspiwack <> | 2018-10-11 09:07:00 (GMT) |
---|---|---|

committer | hdiff <hdiff@hdiff.luite.com> | 2018-10-11 09:07:00 (GMT) |

commit | cc76b23696883665e5dac3d6202f139c7e759c5f (patch) | |

tree | a235533901554b655fb4fe3703ec5728e6cebc62 |

-rw-r--r-- | ChangeLog.md | 5 | ||||

-rw-r--r-- | LICENSE | 30 | ||||

-rw-r--r-- | README.md | 10 | ||||

-rw-r--r-- | Setup.hs | 2 | ||||

-rw-r--r-- | src/Data/Binder/Unfix.hs | 351 | ||||

-rw-r--r-- | unfix-binders.cabal | 24 |

6 files changed, 422 insertions, 0 deletions

diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 index 0000000..fa71fec --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Revision history for unfix-binders + +## 0.1.0 -- 2017-10-10 + +* Bare minimum library, unstable API, for demonstration only @@ -0,0 +1,30 @@ +Copyright (c) 2018, Arnaud Spiwack + +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 Arnaud Spiwack 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/README.md b/README.md new file mode 100644 index 0000000..fc2cc57 --- /dev/null +++ b/README.md @@ -0,0 +1,10 @@ +Unfix binders +============= + +_when your substitutions are in a fix_ + +This library defines fixed points of endofunctors of the category of +endofunctors with the purpose of generalising recursion schemes for +data types with binders. + +It is still in a very experimental state: for demonstration purpose only (though contributions welcome!) diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/Data/Binder/Unfix.hs b/src/Data/Binder/Unfix.hs new file mode 100644 index 0000000..7687aed --- /dev/null +++ b/src/Data/Binder/Unfix.hs @@ -0,0 +1,351 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Binder.Unfix + ( -- * Functors of endofunctors + -- $functor1-and-pfunctor1 + + -- ** Simple functors + -- $functor1 + type (~>) + , Functor1(..) + , Strong1(..) + , Either2(..) + , Var(..) + , Assigned(..) + -- ** Parametric functors + -- $pfunctor1 + , PFunctor1 + -- * Non-uniform fixed point + -- $fixed-points + + -- ** Simple fixed point + -- $mu + , Mu(..) + , cata1 + -- ** Mutually recursive fixed point + -- $mmu + , MMu + , pcata1 + -- * Deriving instances + -- $generic-deriving + + -- ** Deriving 'Functor1' + -- $deriving-functor1 + , GFunctor1 + -- ** Deriving 'Strong1' + -- $deriving-strong1 + , GStrong1 + ) where + +import Data.Kind +import Control.Monad (ap, join) +import GHC.Generics + +-- $functor1-and-pfunctor1 + +-- $functor1 + +-- TODO: doc, explain the restriction for actually being a natural +-- transformation. +type f ~> g = forall a. f a -> g a + +-- TODO: doc, esp. laws +class + (forall f. Functor f => Functor (h f)) + => Functor1 (h :: (* -> *) -> * -> *) + where + fmap1 :: (Functor f, Functor g) => (f ~> g) -> h f ~> h g + + default fmap1 + :: ( Generic1 (h f), Generic1 (h g), GFunctor1 (Rep1 (h f)) (Rep1 (h g)) f g + , Functor f, Functor g ) + => (f ~> g) -> h f ~> h g + fmap1 alpha = to1 . gfmap1 alpha . from1 + +-- TODO: add link to "functorial strength" on wikipedia +-- | The intuition behind @Strong1 h@ is that @h@ acts on monads. Indeed if +-- @f=g=m@ is a monad, then @\x -> strength1 x join :: h m (m a) -> h m a@. This +-- is a limited explanation, but I don't know much more yet. +-- +-- As additional background, for the curious programmer: from a mathematical +-- point of view, 'strenght1' is a functorial strength. For regular functors, a +-- strength is a function @(f a, b) -> f (a, b)@. But for regular functor, there +-- is always such a strength: @\(fa, b) -> (, b) <$> fa@ (this strength is +-- implicitly but critically used in the definition of the do-notation). +-- However functors of endofunctors don't necessarily have a strength (in fact +-- 'Var' below doesn't have one). So we need an additional type class to record +-- that functors are strong. +-- +-- Like in the infamous phrase "a monad is a monoid in the category of +-- endofunctors", the natural product of endofunctors is composition. It is not +-- hard to verify that, up to 'map1', the type of 'strength1' is equivalent to +-- @h f `Compose` g ~> h (f `Compose` g)@. We choose this formulation because it +-- avoids annotations to convert between @Compose f g a@ and @f (g a)@. +-- +-- In any case, this is a natural notion from a mathematics point of view. And +-- not as /ad hoc/ as it may appear at first glance. However, because we +-- wouldn't have interesting instance without it, we restrict @g@ to be an +-- applicative functor. There does not seem to be a need for @f@ to be +-- applicative as well, therefore we depart from usual mathematical practice and +-- only restrict @g@. +class Functor1 h => Strong1 h where + strength1 + :: (Functor f, Applicative g, Functor i) + => h f (g a) -> (forall b. f (g b) -> i b) -> h i a + + default strength1 + :: ( Generic1 (h f), Generic1 (h i), GStrong1 (Rep1 (h f)) (Rep1 (h i)) f g i + , Functor f, Applicative g, Functor i ) + => h f (g a) -> (forall b. f (g b) -> i b) -> h i a + strength1 a alpha = to1 $ gstrength1 (from1 a) alpha + +-- TODO: doc +data Either2 + (h :: (* -> *) -> * -> *) (j :: (* -> *) -> * -> *) (f :: * -> *) (a :: *) + = Left2 (h f a) + | Right2 (j f a) + deriving (Generic1, Functor, Eq) + +instance (Functor1 h, Functor1 j) => Functor1 (Either2 h j) + +instance (Strong1 h, Strong1 j) => Strong1 (Either2 h j) where + +-- TODO: doc, remark that, from an AST point of view, this is the prototypical +-- new thing. Show that this is not strong (/e.g./ Var Identity (Const ()) Void). +data Var (f :: * -> *) (a :: *) = Var a + deriving (Generic1, Functor, Eq) + +instance Functor1 Var where + +-- | @'Assigned' r v a@ represent the computation of a result @r@ parametrised +-- by an assignment of values of type @v@ to each element of @a@. It is a +-- functor (in @a@). +-- +-- Its usefulness derives from the fact that given a 'Functor1' @F@, an algebra +-- of @F@ on @Assigned R V@ yields, via catamorphism (see 'cata1') an algebra of +-- the /monad/ @Mu F@. That is a compositional interpreter for @Mu F@ in the +-- type @R@. This is used /a lot/. +-- +-- You may have noticed that @Assigned r r@ is a monad (the continuation monad +-- @'Cont' r@, in fact). As a matter of fact @Assigned@ is an indexed monad (up, +-- possibly, to the order of its arguments) which is related to delimited +-- continuation. Neither of this fact are useful for our purposes +newtype Assigned (r :: *) (v :: *) (a :: *) = Assigned ((a -> v) -> r) + +instance Functor (Assigned r v) where + fmap f (Assigned from) = Assigned $ \assignment -> from (assignment . f) + +-- $pfunctor1 + +class + (forall f p. (forall q. Functor (f q)) => Functor (h f p)) + => PFunctor1 (h :: (k -> * -> *) -> k -> * -> *) + where + pfmap1 + :: (forall p. Functor (f p), forall q. Functor (g q)) + => (forall q. f q ~> g q) -> h f p ~> h g p + + -- default fmap1 + -- :: ( Generic1 (h f), Generic1 (h g), GFunctor1 (Rep1 (h f)) (Rep1 (h g)) f g + -- , Functor f, Functor g ) + -- => (f ~> g) -> h f ~> h g + -- fmap1 alpha = to1 . gfmap1 alpha . from1 + +-- $fixed-points + +-- $mu + +-- TODO: doc, relation between this and non-uniform data type (example: +-- perfectly balanced binary tree @data Tree a = Leaf a | Node (Tree (a, a)))@) +newtype Mu (h :: (* -> *) -> * -> *) (a :: *) = Roll { unroll :: h (Mu h) a } + +deriving instance (Eq a, forall b f. (Eq b, forall c. Eq c => Eq (f c)) => Eq (h f b)) => Eq (Mu h a) + +instance Functor1 h => Functor (Mu h) where + fmap f (Roll t) = Roll $ fmap f t + +instance Strong1 h => Applicative (Mu (Var `Either2` h)) where + pure x = Roll . Left2 $ Var x + (<*>) = ap + +-- TODO: clearly we should have @Var `Either2` _@ as a macro-operator. +instance Strong1 h => Monad (Mu (Var `Either2` h)) where + t >>= subst = joinTerm $ fmap subst t + where + joinTerm + :: Strong1 h + => Mu (Var `Either2` h) (Mu (Var `Either2` h) a) + -> Mu (Var `Either2` h) a + joinTerm (Roll (Left2 (Var v))) = v + joinTerm (Roll (Right2 u)) = Roll . Right2 $ strength1 u join + +-- TODO: link to catamorphisms, @Mu@ is the initial algebra yadda yadda. +cata1 :: (Functor1 h, Functor f) => (h f ~> f) -> Mu h ~> f +cata1 alg (Roll t) = alg $ fmap1 (cata1 alg) t + +-- ** Mutually recursive fixed point +-- $mmu + +newtype MMu (h :: (k -> * -> *) -> k -> * -> *) (p :: k) (a :: *) + = MRoll {unmroll :: h (MMu h) p a } + +instance PFunctor1 h => Functor (MMu h p) where + fmap f (MRoll t) = MRoll $ fmap f t + +pcata1 + :: (PFunctor1 h, forall q. Functor (f q)) + => (forall q. h f q ~> f q) -> MMu h p ~> f p +pcata1 alg (MRoll t) = alg $ pfmap1 (pcata1 alg) t + +-- $generic-deriving + +-- $deriving-functor1 + +-- TODO: explain what needs to be done to derive things + +-- | A class for deriving 'Functor1' instances generic types. We would really +-- need a @Generic2@ framework (because our types have two arguments). Instead +-- we use an encoding trick, related to the way lenses are defined in the +-- <http://hackage.haskell.org/package/lens lens library>. This trick is due to +-- Csongor Kiss, and documented in +-- <http://kcsongor.github.io/generic-deriving-bifunctor/ this blog post>. +-- +-- The intuition is that the first two argument @h@ and @j@ of the type class, +-- are stand-ins for @h' f@ and @h' g@. +class GFunctor1 (h :: * -> *) (j :: * -> *) (f :: * -> *) (g :: * -> *) where + gfmap1 :: (f ~> g) -> (h ~> j) + +instance {-# INCOHERENT #-} GFunctor1 (Rec1 f) (Rec1 g) f g where + gfmap1 alpha (Rec1 a) = Rec1 $ alpha a + +instance {-# INCOHERENT #-} GFunctor1 (Rec1 i) (Rec1 i) f g where + gfmap1 _ = id + +instance {-# INCOHERENT #-} (Functor1 h, Functor f, Functor g) + => GFunctor1 (Rec1 (h f)) (Rec1 (h g)) f g + where + gfmap1 alpha (Rec1 a) = Rec1 $ fmap1 alpha a + +instance GFunctor1 V1 V1 f g where + gfmap1 _ = id + +instance GFunctor1 U1 U1 f g where + gfmap1 _ = id + +instance GFunctor1 Par1 Par1 f g where + gfmap1 _ = id + +instance GFunctor1 (K1 i c) (K1 i c) g f where + gfmap1 _ = id + +instance GFunctor1 h j f g => GFunctor1 (M1 i c h) (M1 i c j) f g where + gfmap1 alpha (M1 a) = M1 $ gfmap1 alpha a + +instance + (GFunctor1 h1 j1 f g, GFunctor1 h2 j2 f g) + => GFunctor1 (h1 :+: h2) (j1 :+: j2) f g + where + gfmap1 alpha (L1 a) = L1 $ gfmap1 alpha a + gfmap1 alpha (R1 a) = R1 $ gfmap1 alpha a + +instance + (GFunctor1 h1 j1 f g, GFunctor1 h2 j2 f g) + => GFunctor1 (h1 :*: h2) (j1 :*: j2) f g + where + gfmap1 alpha (a :*: b) = gfmap1 alpha a :*: gfmap1 alpha b + +instance + (GFunctor1 h1 j1 f g, GFunctor1 h2 j2 f g, Functor h1) + => GFunctor1 (h1 :.: h2) (j1 :.: j2) f g + where + gfmap1 alpha (Comp1 a) = Comp1 $ gfmap1 alpha (fmap (gfmap1 alpha) a) + +-- For some reason the left-hand side of @:.:@ is not parsed as a 'Rep1', so we +-- need this instance when we recurse on the left-hand side of @:.:@. +instance {-# INCOHERENT #-} GFunctor1 f g f g where + gfmap1 alpha a = alpha a + +-- $deriving-strong1 + +-- TODO: explain what needs to be done to derive things + +-- | A class for deriving 'Strong1' instances generic types. See the +-- documentation of 'Functor1' for details on the encoding. You should read @h@ +-- and @j@ below as being @h' f@ and @h' i@, respectively. +class GStrong1 (h :: * -> *) (j :: * -> *) (f :: * -> *) (g :: * -> *) (i :: * -> *) where + gstrength1 :: h (g a) -> (forall b. f (g b) -> i b) -> j a + +-- TODO: At the moment, I can't find other useful instances for 'Rec1'. Either I +-- will find more, or I will need to give a short explanation as a Haddock +-- comment. +instance {-# INCOHERENT #-} (Strong1 h, Functor f, Applicative g, Functor i) + => GStrong1 (Rec1 (h f)) (Rec1 (h i)) f g i + where + gstrength1 (Rec1 a) alpha = Rec1 $ strength1 a alpha + +instance {-# INCOHERENT #-} GStrong1 (Rec1 f) (Rec1 i) f g i + where + gstrength1 (Rec1 a) alpha = Rec1 $ alpha a + +instance GStrong1 V1 V1 f g i where + gstrength1 v _ = case v of {} + +instance GStrong1 U1 U1 f g i where + gstrength1 U1 _ = U1 + +-- TODO: Turn this into Haddock documentation +-- There is no: +-- +-- > instance GStrong1 Par1 Par1 f g i where +-- +-- As it would require a function @g a -> a@. Such as if @g@ is a comonad. But +-- 'Strong1' is abstract over @g@, so this would not be useful. + +instance GStrong1 (K1 m c) (K1 m c) g f i where + gstrength1 (K1 c) _ = K1 c + +instance GStrong1 h j f g i => GStrong1 (M1 m c h) (M1 m c j) f g i where + gstrength1 (M1 a) alpha = M1 $ gstrength1 a alpha + +instance + (GStrong1 h1 j1 f g i, GStrong1 h2 j2 f g i) + => GStrong1 (h1 :+: h2) (j1 :+: j2) f g i + where + gstrength1 (L1 a) alpha = L1 $ gstrength1 a alpha + gstrength1 (R1 a) alpha = R1 $ gstrength1 a alpha + +instance + (GStrong1 h1 j1 f g i, GStrong1 h2 j2 f g i) + => GStrong1 (h1 :*: h2) (j1 :*: j2) f g i + where + gstrength1 (a :*: b) alpha = gstrength1 a alpha :*: gstrength1 b alpha + +instance + (GStrong1 h1 j1 f g i, Traversable t, Functor h1, Traversable t, Applicative g) + => GStrong1 (h1 :.: t) (j1 :.: t) f g i + where + gstrength1 (Comp1 a) alpha = Comp1 $ gstrength1 (fmap sequenceA a) alpha + +-- For some reason the left-hand side of @:.:@ is not parsed as a 'Rep1', so we +-- need this instance when we recurse on the left-hand side of @:.:@. +instance {-# INCOHERENT #-} GStrong1 f i f g i + where + gstrength1 a alpha = alpha a + + +-- LocalWords: monads monad functorial functor functors endofunctors monoid +-- LocalWords: comonad applicative diff --git a/unfix-binders.cabal b/unfix-binders.cabal new file mode 100644 index 0000000..1eb1bef --- /dev/null +++ b/unfix-binders.cabal @@ -0,0 +1,24 @@ +-- Initial unfix-binders.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: unfix-binders +version: 0.1.0 +synopsis: Unfixing and recursion schemes for data types with binders +description: Use fixed-point of endofunctors of endofunctors (that is initial algebras in the category of endofunctors) to define recursion schemes for data types with binders +homepage: https://github.com/aspiwack/peppermint-prover +license: BSD3 +license-file: LICENSE +author: Arnaud Spiwack +maintainer: arnaud@spiwack.net +copyright: 2018 Arnaud Spiwack +category: Data +build-type: Simple +extra-source-files: README.md, ChangeLog.md +cabal-version: >=1.10 + +library + exposed-modules: + Data.Binder.Unfix + build-depends: base >=4.12 && <4.13 + hs-source-dirs: src + default-language: Haskell2010 |