diff --git a/changelog.md b/changelog.md new file mode 100644 --- /dev/null +++ b/changelog.md @@ -0,0 +1,3 @@ + +# Versions 0.1.0.0 - 0.1.0.2 +initial release(s) with only the private proof rep for tree paths diff --git a/resin.cabal b/resin.cabal --- a/resin.cabal +++ b/resin.cabal @@ -10,7 +10,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change -version: 0.1.0.2 +version: 0.2.0.0 -- A short (one-line) description of the package. synopsis: High performance variable binders @@ -46,7 +46,8 @@ -- Extra files to be distributed with the package, such as examples or a -- README. -extra-source-files: readme.md +extra-source-files: readme.md + changelog.md @@ -62,8 +63,8 @@ exposed-modules: -- Resin - -- , Resin.Binders.Tree + ,Resin.Binders.Tree.Internal -- ,Resin.Calculus.Derivatives @@ -76,9 +77,11 @@ -- other-extensions: -- Other library packages from which modules are imported. - build-depends: base >=4.8 && <4.11 - ,ghc-prim >= 0.4 && < 0.6 + build-depends: base >= 4.8 && < 4.12 + ,ghc-prim + -- >= 0.4 && < 0.6 ,semigroupoids >= 5.0 && < 5.3 + ,ralist == 0.2.* -- Directories containing source files. @@ -86,8 +89,6 @@ ghc-options: -Wall - if impl(ghc >= 8.0) && impl(ghc < 8.2) - ghc-options: -Wcompat -Wnoncanonical-monad-instances -Wnoncanonical-monadfail-instances if impl(ghc >= 8.0) && impl(ghc < 8.2) ghc-options: -Wno-redundant-constraints diff --git a/src/Resin/Binders/Tree.hs b/src/Resin/Binders/Tree.hs --- a/src/Resin/Binders/Tree.hs +++ b/src/Resin/Binders/Tree.hs @@ -1,101 +1,16 @@ -{-# LANGUAGE FlexibleContexts,FlexibleInstances,GADTs,DataKinds, PolyKinds, KindSignatures #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE TypeOperators #-} - -module Resin.Binders.Tree where -import Data.Kind -import Numeric.Natural -import Data.Semigroupoid ---import Data.Coerce -import Unsafe.Coerce (unsafeCoerce) -import Data.Type.Equality ---import qualified Data.Semigroupoid.Dual as DL - - -{- -This module models binders which respect scope having a tree shaped topology -or at least it models some ideas about (finite?) paths on (finite??!) trees - --} - - -data IxEq :: (k -> Type ) -> k -> k -> Type where - PolyRefl :: IxEq f i i - MonoRefl :: forall f i . f i -> IxEq f i i - ---testIxEquality :: TestEquality f => IxEq f a b -> IxEq f b c -> - -instance TestEquality f => TestEquality (IxEq f i) where - testEquality (MonoRefl f1) (MonoRefl f2) = testEquality f1 f2 - testEquality (PolyRefl )(MonoRefl _f2) = Just Refl - testEquality (MonoRefl _f1) (PolyRefl ) = Just Refl - testEquality (PolyRefl ) (PolyRefl ) = Just Refl - -{- | `Inject` is about - --} -data Inject :: (k -> Type ) -> k -> k -> Type where - InjectRefl :: forall f a b . IxEq f a b-> Inject f a b - --MonoId :: forall f i . (f i) -> Inject f i i - -- should MonoId be strict in its argument? - CompactCompose :: forall f i j . (IxEq f i i) -> (IxEq f j j ) -> Natural -> Inject f i j - -- i is origin/root - -- j is leaf - -- compact compose is unsafe for users, but should be exposed in a .Internal - -- module - - - -instance Semigroupoid (Inject f) where - --PolyId `o` PolyId = PolyId - (InjectRefl (MonoRefl _p)) `o` (!f) = f - (InjectRefl (PolyRefl)) `o` (!f) = f - (CompactCompose in1 out1 size) `o` (InjectRefl (PolyRefl)) = CompactCompose in1 out1 size - (CompactCompose in1 out1 size) `o` (InjectRefl (MonoRefl !_p)) = CompactCompose in1 out1 size - (CompactCompose _cmiddle2 cout sizeleft) - `o` (CompactCompose cin _cmiddle1 sizeright) = CompactCompose cin cout (sizeright + sizeleft) - --- TODO is this case to lazy? - --- extract is the dual of Inject --- aka Data.Semigroupoid.Dual is nearly the exact same type :) -newtype Extract :: (k -> Type ) -> k -> k -> Type where - Dual :: ((Inject f) b a ) -> Extract f a b --- not sure if this is the right design vs - -- :: Inject f b a -> Extract f a b --- (which has more explicit duality and less newtypery) - - -instance Semigroupoid (Extract f) where - o = \ (Dual l) (Dual r) -> Dual $ r `o` l - - -data TreeEq :: (k -> Type ) -> k -> k -> Type where - TreeInject :: Inject f a b -> TreeEq f a b - TreeExtract :: Extract f a b -> TreeEq f a b - TreeRefl :: TreeEq f c c - - ---- this might limit a,c to being kind (or sort?) * / Type for now, but thats OK ?? -treeElimination :: TestEquality f => Inject f a b -> Extract f b c-> (TreeEq f a c) -treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl PolyRefl)) = TreeRefl -treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl PolyRefl)) = TreeRefl -treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl (MonoRefl _p2))) = TreeRefl -treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl(MonoRefl _p2))) = TreeRefl -treeElimination (CompactCompose fa _fb1 n1) (Dual (CompactCompose fc _fb2 n2)) = - case (compare n1 n2, max n1 n2 - min n1 n2) of - (EQ, _ )-> (unsafeCoerce TreeRefl) :: TreeEq f a c - --- if the path is zero length they must be equal! - --- AUDIT MEEEE - (GT, m )-> TreeInject (CompactCompose fa fc m) - (LT, m ) -> TreeExtract (Dual (CompactCompose fc fa m)) -treeElimination (InjectRefl p@(PolyRefl)) - d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d -treeElimination (InjectRefl p@(MonoRefl _)) - d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d -treeElimination d@( CompactCompose _fc _fb _n) - (Dual (InjectRefl p@(PolyRefl))) = treeElimination d (Dual (CompactCompose p p 0)) -treeElimination d@(CompactCompose _fc _fb _n) - (Dual (InjectRefl p@(MonoRefl _))) = treeElimination d (Dual (CompactCompose p p 0)) +{-# LANGUAGE Trustworthy #-} +module Resin.Binders.Tree( + -- | the safe subset of the api... I think + IxEq(..) + ,Inject(InjectRefl) + ,Extract -- Extract is just a newtype wrapper .. for now + ,TreeEq(..) + ,treeElimination + ,rightExtendInject + ,leftExtendExtract + ,jumpDepthInject -- not sure if this operation is safe + ,jumpDepthExtract -- not sure if thats safe too + ) + where +import Resin.Binders.Tree.Internal diff --git a/src/Resin/Binders/Tree/Internal.hs b/src/Resin/Binders/Tree/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Resin/Binders/Tree/Internal.hs @@ -0,0 +1,129 @@ +{-# LANGUAGE FlexibleContexts,FlexibleInstances,GADTs,DataKinds, PolyKinds, KindSignatures #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE TypeOperators #-} + +module Resin.Binders.Tree.Internal( + -- | the safe subset of the api... I think + IxEq(..) + ,Inject(..) + ,Extract(..) -- Extract is just a newtype wrapper .. for now + ,TreeEq(..) + ,treeElimination + ,rightExtendInject + ,leftExtendExtract + ,jumpDepthInject -- not sure if this operation is safe + ,jumpDepthExtract -- not sure if thats safe too + ) where +import Data.Kind +import Numeric.Natural +import Data.Semigroupoid +--import Data.Coerce +import Unsafe.Coerce (unsafeCoerce) +import Data.Type.Equality +--import qualified Data.Semigroupoid.Dual as DL + + + + +{- +This module models binders which respect scope having a tree shaped topology +or at least it models some ideas about (finite?) paths on (finite??!) trees + +-} + + +data IxEq :: (k -> Type ) -> k -> k -> Type where + PolyRefl :: IxEq f i i + MonoRefl :: forall f i . f i -> IxEq f i i + +--testIxEquality :: TestEquality f => IxEq f a b -> IxEq f b c -> + +instance TestEquality f => TestEquality (IxEq f i) where + testEquality (MonoRefl f1) (MonoRefl f2) = testEquality f1 f2 + testEquality (PolyRefl )(MonoRefl _f2) = Just Refl + testEquality (MonoRefl _f1) (PolyRefl ) = Just Refl + testEquality (PolyRefl ) (PolyRefl ) = Just Refl + +{- | `Inject` is about + +-} +data Inject :: (k -> Type ) -> k -> k -> Type where + InjectRefl :: forall f a b . IxEq f a b-> Inject f a b + --MonoId :: forall f i . (f i) -> Inject f i i + -- should MonoId be strict in its argument? + CompactCompose :: forall f i j . (IxEq f i i) -> (IxEq f j j ) -> Natural -> Inject f i j + -- i is origin/root + -- j is leaf + -- compact compose is unsafe for users, but should be exposed in a .Internal + -- module + +rightExtendInject :: Inject p a b -> p c -> Inject p a c +rightExtendInject (InjectRefl PolyRefl) rP = CompactCompose PolyRefl (MonoRefl rP) 1 +rightExtendInject (InjectRefl (MonoRefl f)) rP = CompactCompose (MonoRefl f) (MonoRefl rP) 1 +rightExtendInject (CompactCompose pa _pb n) rP = CompactCompose pa (MonoRefl rP) (n+1 ) + +leftExtendExtract :: p a -> Extract p b c -> Extract p a c +leftExtendExtract p (Dual inj) = Dual (rightExtendInject inj p) + + +jumpDepthInject :: Natural -> p c -> Inject p a b -> Inject p a c +jumpDepthInject plus pc (InjectRefl PolyRefl) = CompactCompose PolyRefl (MonoRefl pc) (1 + plus) +jumpDepthInject plus pc (InjectRefl (MonoRefl pa)) = CompactCompose (MonoRefl pa) (MonoRefl pc) (1 + plus) +jumpDepthInject plus pc (CompactCompose pa _pb n) = CompactCompose pa (MonoRefl pc) (n + plus + 1 ) + +jumpDepthExtract :: Natural -> Extract p b c -> p a -> Extract p a c +jumpDepthExtract plus (Dual cc) pc = Dual (jumpDepthInject plus pc cc) + +instance Semigroupoid (Inject f) where + --PolyId `o` PolyId = PolyId + (InjectRefl (MonoRefl _p)) `o` (!f) = f + (InjectRefl (PolyRefl)) `o` (!f) = f + (CompactCompose in1 out1 size) `o` (InjectRefl (PolyRefl)) = CompactCompose in1 out1 size + (CompactCompose in1 out1 size) `o` (InjectRefl (MonoRefl !_p)) = CompactCompose in1 out1 size + (CompactCompose _cmiddle2 cout sizeleft) + `o` (CompactCompose cin _cmiddle1 sizeright) = CompactCompose cin cout (sizeright + sizeleft) + --- TODO is this case too lazy? + +-- extract is the dual of Inject +-- aka Data.Semigroupoid.Dual is nearly the exact same type :) +newtype Extract :: (k -> Type ) -> k -> k -> Type where + Dual :: ((Inject f) b a ) -> Extract f a b +-- not sure if this is the right design vs + -- :: Inject f b a -> Extract f a b --- (which has more explicit duality and less newtypery) + + +instance Semigroupoid (Extract f) where + o = \ (Dual l) (Dual r) -> Dual $ r `o` l + + +data TreeEq :: (k -> Type ) -> k -> k -> Type where + TreeInject :: Inject f a b -> TreeEq f a b + TreeExtract :: Extract f a b -> TreeEq f a b + TreeRefl :: TreeEq f c c + + +--- this might limit a,c to being kind (or sort?) * / Type for now, but thats OK ?? +treeElimination :: TestEquality f => Inject f a b -> Extract f b c-> (TreeEq f a c) +treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl PolyRefl)) = TreeRefl +treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl PolyRefl)) = TreeRefl +treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl (MonoRefl _p2))) = TreeRefl +treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl(MonoRefl _p2))) = TreeRefl +treeElimination (CompactCompose fa _fb1 n1) (Dual (CompactCompose fc _fb2 n2)) = + case (compare n1 n2, max n1 n2 - min n1 n2) of + (EQ, _ )-> (unsafeCoerce TreeRefl) :: TreeEq f a c + --- if the path is zero length they must be equal! + --- AUDIT MEEEE + (GT, m )-> TreeInject (CompactCompose fa fc m) + (LT, m ) -> TreeExtract (Dual (CompactCompose fc fa m)) +treeElimination (InjectRefl p@(PolyRefl)) + d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d +treeElimination (InjectRefl p@(MonoRefl _)) + d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d +treeElimination d@( CompactCompose _fc _fb _n) + (Dual (InjectRefl p@(PolyRefl))) = treeElimination d (Dual (CompactCompose p p 0)) +treeElimination d@(CompactCompose _fc _fb _n) + (Dual (InjectRefl p@(MonoRefl _))) = treeElimination d (Dual (CompactCompose p p 0)) +