diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,26 @@ +Copyright (c) 2016, Carter Tazio Schonwald +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are +met: + +1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + +2. 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. + +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 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/readme.md b/readme.md new file mode 100644 --- /dev/null +++ b/readme.md @@ -0,0 +1,9 @@ +# Resin : High performance Planar (2D) Variable binders + +Resin is an experiment in variable binder design inspired by binder libraries +such as Bound and UnBound (no relation), with the goal being to provide +high performance and excellent abstraction on as large a space of syntaxes as +is feasible. + + + diff --git a/resin.cabal b/resin.cabal new file mode 100644 --- /dev/null +++ b/resin.cabal @@ -0,0 +1,96 @@ +-- Initial resin.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/ + +-- The name of the package. +name: resin + +-- The package version. See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented. +-- http://www.haskell.org/haskellwiki/Package_versioning_policy +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.1.0.0 + +-- A short (one-line) description of the package. +synopsis: High performance variable binders + +-- A longer description of the package. +description: High Performance Variable Binders library + +-- URL for the project homepage or repository. +homepage: http://github.com/cartazio/resin + + +-- The license under which the package is released. +license: BSD2 + +-- The file containing the license text. +license-file: LICENSE + +-- The package author(s). +author: Carter Tazio Schonwald + +-- An email address to which users can send suggestions, bug reports, and +-- patches. +maintainer: carter at wellposed dot com + +-- A copyright notice. +-- copyright: + +category: Language + +build-type: Simple + + + +-- Extra files to be distributed with the package, such as examples or a +-- README. +extra-source-files: readme.md + + + +-- Constraint on the version of Cabal needed to build this package. +cabal-version: >=1.10 + +source-repository head + type: git + location: https://github.com/cartazio/ralist.git + +library + -- Modules exported by the library. + exposed-modules: + -- Resin + + -- , + Resin.Binders.Tree + + -- ,Resin.Calculus.Derivatives + + -- ,Resin.Environment.Class + + -- Modules included in this library but not exported. + -- other-modules: + + -- LANGUAGE extensions used by modules in this package. + -- other-extensions: + + -- Other library packages from which modules are imported. + build-depends: base >=4.8 && <4.11 + ,ghc-prim >= 0.4 && < 0.6 + ,semigroupoids >= 5.0 && < 5.3 + + + -- Directories containing source files. + hs-source-dirs: src + 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 + else + -- provide/emulate `Control.Monad.Fail` and `Data.Semigroups` API for pre-GHC8 + build-depends: fail == 4.9.*, semigroups == 0.18.* + ghc-options: -Wall + -- Base language which the package is written in. + default-language: Haskell2010 + diff --git a/src/Resin/Binders/Tree.hs b/src/Resin/Binders/Tree.hs new file mode 100644 --- /dev/null +++ b/src/Resin/Binders/Tree.hs @@ -0,0 +1,101 @@ +{-# 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)) +