Initial commit

.gitignore

@@ -0,0 +1,2 @@
+.stack-work
+

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2017 Joshua Moerman
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

README.md

@@ -0,0 +1,31 @@
+# ons-hs
+
+Experimental implemtation of the ONS library in Haskell. It provides the basic
+notion of nominal sets and maps, and their manipulations (over the total order
+symmetry). It is implemented by instantiating the known representation theory,
+which turns out to be quite easy for the total order symmetry.
+
+Nominal sets are structured possibly-infinite sets. They have symmetries which
+make them finitely representable. They can be used, for example, to define
+infinite state systems (nominal automata). Consequently, one can then do
+reachability analysis, minimisation and other automata-theoretic constructions.
+Here we take nominal sets over the total order symmetry, which means that the
+data-values come from the rational numbers (or any other dense linear order).
+The symmetries which act upon the nominal sets are the monotone bijections on
+the rationals.
+
+The library uses an interface similar to the one provided by
+[ONS](https://github.com/davidv1992/ONS). It provides basic instances and also
+allows custom types to be nominal. It is purely functional.
+
+
+## TODO
+
+This will never be a fully fledged library. It is just for fun. Nevertheless, I
+wish to do the following:
+
+* Provide generic instances
+* Figure out the right data-structures (List vs. Sets vs. Seqs vs. ...)
+* Cleanup
+* Examples
+* Tests

Setup.hs

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

app/Main.hs

@@ -0,0 +1,6 @@
+module Main where
+
+import Orbit
+
+main :: IO ()
+main = putStrLn "Hello from App.hs"

ons-hs.cabal

@@ -0,0 +1,44 @@
+name:                ons-hs
+version:             0.1.0.0
+synopsis:            Implementation of the ONS (Ordered Nominal Sets) library in Haskell
+description:         Nominal sets are structured infinite sets. They have symmetries which make them finitely representable. This library provides basic manipulation of them for the total order symmetry. It includes: products, sums, maps and sets. Can work with custom data types.
+homepage:            https://gitlab.science.ru.nl/moerman/ons-hs
+license:             MIT
+license-file:        LICENSE
+author:              Joshua Moerman
+maintainer:          haskell@joshuamoerman.nl
+copyright:           Joshua Moerman
+category:            Unclassified
+build-type:          Simple
+extra-source-files:  README.md
+cabal-version:       >=1.10
+
+library
+  hs-source-dirs:      src
+  exposed-modules:     EquivariantMap
+                     , EquivariantSet
+                     , Orbit
+  build-depends:       base >= 4.7 && < 5
+                     , containers
+  default-language:    Haskell2010
+
+executable ons-hs-exe
+  hs-source-dirs:      app
+  main-is:             Main.hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  build-depends:       base
+                     , ons-hs
+  default-language:    Haskell2010
+
+test-suite ons-hs-test
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             Spec.hs
+  build-depends:       base
+                     , ons-hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  default-language:    Haskell2010
+
+source-repository head
+  type:     git
+  location: https://gitlab.science.ru.nl/moerman/ons-hs

src/EquivariantMap.hs

@@ -0,0 +1,119 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module EquivariantMap where
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Semigroup (Semigroup)
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+import EquivariantSet (EquivariantSet(EqSet))
+import Orbit
+
+-- Very similar to EquivariantSet
+-- Some of the notes there apply here too
+newtype EquivariantMap k v = EqMap { unEqMap :: Map (Orb k) (Orb v, [Bool]) }
+
+-- Need undecidableIntances for this
+deriving instance (Eq (Orb k), Eq (Orb v)) => Eq (EquivariantMap k v)
+deriving instance (Ord (Orb k), Ord (Orb v)) => Ord (EquivariantMap k v)
+deriving instance (Show (Orb k), Show (Orb v)) => Show (EquivariantMap k v)
+
+-- Left biased...
+deriving instance Ord (Orb k) => Monoid (EquivariantMap k v)
+deriving instance Ord (Orb k) => Semigroup (EquivariantMap k v)
+
+-- TODO: foldable / traversable
+-- TODO: adjust / alter / update
+-- TODO: *WithKey functions
+
+-- Some helper functions
+-- TODO: don't export these
+
+mapel :: (Orbit k, Orbit v) => k -> v -> (Orb v, [Bool])
+mapel k v = (toOrbit v, bv (Set.toAscList (support k)) (Set.toAscList (support v)))
+
+bv :: [Rat] -> [Rat] -> [Bool]
+bv l [] = replicate (length l) False
+bv [] l = undefined -- Non-equivariant function
+bv (x:xs) (y:ys) = case compare x y of
+  LT -> False : bv xs (y:ys)
+  EQ -> True : bv xs ys
+  GT -> undefined -- Non-equivariant function
+
+mapelInv :: (Orbit k, Orbit v) => k -> (Orb v, [Bool]) -> v
+mapelInv x (oy, bv) = getElement oy (Set.fromAscList . fmap fst . Prelude.filter snd $ zip (Set.toAscList (support x)) bv)
+
+
+-- Query
+
+null :: EquivariantMap k v -> Bool
+null (EqMap m) = Map.null m
+
+member :: (Orbit k, Ord (Orb k)) => k -> EquivariantMap k v -> Bool
+member x (EqMap m) = Map.member (toOrbit x) m
+
+lookup :: (Orbit k, Ord (Orb k), Orbit v) => k -> EquivariantMap k v -> Maybe v
+lookup x (EqMap m) = mapelInv x <$> Map.lookup (toOrbit x) m
+
+
+-- Construction
+
+empty :: EquivariantMap k v
+empty = EqMap Map.empty
+
+singleton :: (Orbit k, Orbit v) => k -> v -> EquivariantMap k v
+singleton k v = EqMap (Map.singleton (toOrbit k) (mapel k v))
+
+insert :: (Orbit k, Orbit v, Ord (Orb k)) => k -> v -> EquivariantMap k v -> EquivariantMap k v
+insert k v (EqMap m) = EqMap (Map.insert (toOrbit k) (mapel k v) m)
+
+delete :: (Orbit k, Ord (Orb k)) => k -> EquivariantMap k v -> EquivariantMap k v
+delete k (EqMap m) = EqMap (Map.delete (toOrbit k) m)
+
+
+-- Combine
+
+-- Can be done with just Map.unionWith and without getElementE but is a bit
+-- harder (probably easier). Also true for related functions
+-- op should be equivariant!
+unionWith :: (Orbit k, Orbit v, Ord (Orb k)) => (v -> v -> v) -> EquivariantMap k v -> EquivariantMap k v -> EquivariantMap k v
+unionWith op (EqMap m1) (EqMap m2) = EqMap (Map.unionWithKey opl m1 m2)
+  where opl ko p1 p2 = let k = getElementE ko in mapel k (mapelInv k p1 `op` mapelInv k p2)
+
+intersectionWith :: (Orbit k, Orbit v1, Orbit v2, Orbit v3, Ord (Orb k)) => (v1 -> v2 -> v3) -> EquivariantMap k v1 -> EquivariantMap k v2 -> EquivariantMap k v3
+intersectionWith op (EqMap m1) (EqMap m2) = EqMap (Map.intersectionWithKey opl m1 m2)
+  where opl ko p1 p2 = let k = getElementE ko in mapel k (mapelInv k p1 `op` mapelInv k p2)
+
+
+-- Traversal
+
+-- f should be equivariant
+map :: (Orbit k, Orbit v1, Orbit v2) => (v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2
+map f (EqMap m) = EqMap (Map.mapWithKey f2 m)
+  where f2 ko p1 = let k = getElementE ko in mapel k (f $ mapelInv k p1)
+
+mapWithKey :: (Orbit k, Orbit v1, Orbit v2) => (k -> v1 -> v2) -> EquivariantMap k v1 -> EquivariantMap k v2
+mapWithKey f (EqMap m) = EqMap (Map.mapWithKey f2 m)
+  where f2 ko p1 = let k = getElementE ko in mapel k (f k $ mapelInv k p1)
+
+
+-- Conversion
+
+keysSet :: EquivariantMap k v -> EquivariantSet k
+keysSet (EqMap m) = EqSet (Map.keysSet m)
+
+fromSet :: (Orbit k, Orbit v) => (k -> v) -> EquivariantSet k -> EquivariantMap k v
+fromSet f (EqSet s) = EqMap (Map.fromSet f2 s)
+  where f2 ko = let k = getElementE ko in mapel k (f k)
+
+
+-- Filter
+
+filter :: (Orbit k, Orbit v) => (v -> Bool) -> EquivariantMap k v -> EquivariantMap k v
+filter p (EqMap m) = EqMap (Map.filterWithKey p2 m)
+  where p2 ko pr = let k = getElementE ko in p $ mapelInv k pr

src/EquivariantSet.hs

@@ -0,0 +1,103 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module EquivariantSet where
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Semigroup (Semigroup)
+
+import Orbit
+
+-- Given a nominal type, we can construct equivariant sets
+-- These simply use a set data structure from prelude
+-- This works well because orbits are uniquely represented
+-- Note that functions such as toList do not return an ordered
+-- list since the representatives are chosen arbitrarily.
+-- TODO: think about folds (and size)
+newtype EquivariantSet a = EqSet { unEqSet :: Set (Orb a) }
+
+-- Need undecidableIntances for this
+deriving instance Eq (Orb a) => Eq (EquivariantSet a)
+deriving instance Ord (Orb a) => Ord (EquivariantSet a)
+deriving instance Show (Orb a) => Show (EquivariantSet a)
+
+-- For these we rely on the instances of Set
+-- It defines the join semi-lattice structure
+deriving instance Ord (Orb a) => Monoid (EquivariantSet a)
+deriving instance Ord (Orb a) => Semigroup (EquivariantSet a)
+
+
+-- Query
+
+null :: EquivariantSet a -> Bool
+null = Set.null . unEqSet
+
+size :: EquivariantSet a -> Int
+size = Set.size . unEqSet
+
+member :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> Bool
+member a = Set.member (toOrbit a) . unEqSet
+
+isSubsetOf :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> Bool
+isSubsetOf (EqSet s1) (EqSet s2) = Set.isSubsetOf s1 s2
+
+
+-- Construction
+
+empty :: EquivariantSet a
+empty = EqSet Set.empty
+
+singleOrbit :: Orbit a => a -> EquivariantSet a
+singleOrbit = EqSet . Set.singleton . toOrbit
+
+insert :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> EquivariantSet a
+insert a = EqSet . Set.insert (toOrbit a) . unEqSet
+
+delete :: (Orbit a, Ord (Orb a)) => a -> EquivariantSet a -> EquivariantSet a
+delete a = EqSet . Set.delete (toOrbit a) . unEqSet
+
+
+-- Combine
+
+union :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
+union a b = EqSet $ Set.union (unEqSet a) (unEqSet b)
+
+difference :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
+difference a b = EqSet $ Set.difference (unEqSet a) (unEqSet b)
+
+intersection :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
+intersection a b = EqSet $ Set.intersection (unEqSet a) (unEqSet b)
+
+-- This is the meat of the file!
+product :: (Orbit a, Orbit b) => EquivariantSet a -> EquivariantSet b -> EquivariantSet (a, b)
+product (EqSet sa) (EqSet sb) = EqSet . Set.fromDistinctAscList . concat
+                              $ Orbit.product <$> Set.toAscList sa <*> Set.toAscList sb
+
+
+-- Filter
+
+-- f should be equivariant
+filter :: Orbit a => (a -> Bool) -> EquivariantSet a -> EquivariantSet a
+filter f (EqSet s) = EqSet . Set.filter (f . getElementE) $ s
+
+
+-- Map
+
+-- precondition: f is equivariant
+-- Note that f may change the ordering
+map :: (Orbit a, Orbit b, Ord (Orb b)) => (a -> b) -> EquivariantSet a -> EquivariantSet b
+map f = EqSet . Set.map (toOrbit . f . getElementE) . unEqSet
+
+-- f should also preserve order!
+mapMonotonic :: (Orbit a, Orbit b) => (a -> b) -> EquivariantSet a -> EquivariantSet b
+mapMonotonic f = EqSet . Set.mapMonotonic (toOrbit . f . getElementE) . unEqSet
+
+
+-- Conversion
+
+toList :: Orbit a => EquivariantSet a -> [a]
+toList = fmap getElementE . Set.toList . unEqSet
+

src/Orbit.hs

@@ -0,0 +1,149 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Orbit where
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+-- We only need ordering on this structure
+-- I wrap it, because Rational is a type synonym
+newtype Rat = Rat { unRat :: Rational }
+  deriving (Eq, Ord)
+
+-- Just for debugging
+instance Show Rat where
+  show (Rat r) = show r
+  showsPrec n (Rat r) = showsPrec n r
+
+-- A support is a set of rational numbers
+-- Can also be represented as sorted list/vector
+-- I should experiment with that, once I have some tests
+type Support = Set Rat
+
+-- Type class indicating that we can associate orbits with elements
+-- In fact, it means that a is a nominal type
+class Orbit a where
+  data Orb a :: *
+  toOrbit :: a -> Orb a
+  support :: a -> Support
+  -- Precondition: size of set == index
+  getElement :: Orb a -> Support -> a
+  -- Size of least support
+  index :: Orb a -> Int
+
+-- Just some element
+getElementE :: Orbit a => Orb a -> a
+getElementE orb = getElement orb (Set.fromAscList . fmap (Rat . toRational) $ [1 .. index orb])
+
+-- Rational numbers fit the bill
+instance Orbit Rat where
+  data Orb Rat = OrbRational
+  toOrbit _ = OrbRational
+  support r = Set.singleton r
+  getElement _ s
+    | Set.null s = undefined
+    | otherwise = Set.findMin s
+  index _ = 1
+
+deriving instance Show (Orb Rat)
+deriving instance Eq (Orb Rat)
+deriving instance Ord (Orb Rat)
+
+-- Cartesian product of nominal sets as well
+-- TODO: replace [Ordering] with Vec Ordering if better
+instance (Orbit a, Orbit b) => Orbit (a, b) where
+  data Orb (a,b) = OrbPair !(Orb a) !(Orb b) ![Ordering]
+  toOrbit (a, b) = OrbPair (toOrbit a) (toOrbit b) (bla sa sb) 
+    where
+      sa = Set.toAscList $ support a
+      sb = Set.toAscList $ support b
+      bla [] ys = fmap (const GT) ys
+      bla xs [] = fmap (const LT) xs
+      bla (x:xs) (y:ys) = case compare x y of
+        LT -> LT : (bla xs (y:ys))
+        EQ -> EQ : (bla xs ys)
+        GT -> GT : (bla (x:xs) ys)
+  support (a, b) = Set.union (support a) (support b)
+  getElement (OrbPair oa ob l) s = (getElement oa $ toSet ls, getElement ob $ toSet rs)
+    where
+      (ls, rs) = partitionOrd fst . zip l . Set.toAscList $ s
+      toSet = Set.fromAscList . fmap snd
+  index (OrbPair _ _ l) = length l
+
+deriving instance (Show (Orb a), Show (Orb b)) => Show (Orb (a, b))
+deriving instance (Eq (Orb a), Eq (Orb b)) => Eq (Orb (a, b))
+deriving instance (Ord (Orb a), Ord (Orb b)) => Ord (Orb (a, b))
+
+-- Could be in prelude or some other general purpose lib
+partitionOrd :: (a -> Ordering) -> [a] -> ([a],[a])
+{-# INLINE partitionOrd #-}
+partitionOrd p xs = foldr (selectOrd p) ([], []) xs
+
+selectOrd :: (a -> Ordering) -> a -> ([a], [a]) -> ([a], [a])
+selectOrd f x ~(ls, rs) = case f x of
+  LT -> (x : ls, rs)
+  EQ -> (x : ls, x : rs)
+  GT -> (ls, x : rs)
+
+-- Enumerate all orbits in a product
+-- In lexicographical order
+product :: (Orbit a, Orbit b) => Orb a -> Orb b -> [Orb (a, b)]
+product oa ob = OrbPair oa ob <$> prodStrings (index oa) (index ob)
+
+prodStrings :: Int -> Int -> [[Ordering]]
+prodStrings 0 0 = [[]]
+prodStrings 0 n = [replicate n GT]
+prodStrings n 0 = [replicate n LT]
+prodStrings 1 1 = [[LT, GT], [EQ], [GT, LT]]
+prodStrings n m = ((LT :) <$> prodStrings (n-1) m)
+  ++ ((EQ :) <$> prodStrings (n-1) (m-1))
+  ++ ((GT :) <$> prodStrings n (m-1))
+
+-- Also for sums
+instance (Orbit a, Orbit b) => Orbit (Either a b) where
+  newtype Orb (Either a b) = OrbEither (Either (Orb a) (Orb b))
+  toOrbit (Left a) = OrbEither (Left (toOrbit a))
+  toOrbit (Right b) = OrbEither (Right (toOrbit b))
+  support (Left a) = support a
+  support (Right b) = support b
+  getElement (OrbEither (Left oa)) s = Left (getElement oa s)
+  getElement (OrbEither (Right ob)) s = Right (getElement ob s)
+  index (OrbEither (Left oa)) = index oa
+  index (OrbEither (Right ob)) = index ob
+
+deriving instance (Show (Orb a), Show (Orb b)) => Show (Orb (Either a b))
+deriving instance (Eq (Orb a), Eq (Orb b)) => Eq (Orb (Either a b))
+deriving instance (Ord (Orb a), Ord (Orb b)) => Ord (Orb (Either a b))
+
+-- Data structure for the discrete nominal sets
+-- with a trivial action.
+data Trivial a = Trivial { unTrivial :: a }
+
+-- We need to remember the value!
+instance Orbit (Trivial a) where
+  newtype Orb (Trivial a) = OrbTrivial a
+  toOrbit (Trivial a) = OrbTrivial a
+  support _ = Set.empty
+  getElement (OrbTrivial a) _ = Trivial a
+  index _ = 0
+
+deriving instance Show a => Show (Orb (Trivial a))
+deriving instance Eq a => Eq (Orb (Trivial a))
+deriving instance Ord a => Ord (Orb (Trivial a))
+
+-- Orbits themselves are trivial,
+-- but we need to keep track of the orbit
+instance Orbit a => Orbit (Orb a) where
+  newtype Orb (Orb a) = OrbOrb (Orb a)
+  toOrbit a = OrbOrb a
+  support _ = Set.empty
+  getElement (OrbOrb oa) _ = oa
+  index _ = 0
+
+-- These are funny looking...
+deriving instance Show (Orb a) => Show (Orb (Orb a))
+deriving instance Eq (Orb a) => Eq (Orb (Orb a))
+deriving instance Ord (Orb a) => Ord (Orb (Orb a))

stack.yaml

@@ -0,0 +1,66 @@
+# This file was automatically generated by 'stack init'
+#
+# Some commonly used options have been documented as comments in this file.
+# For advanced use and comprehensive documentation of the format, please see:
+# https://docs.haskellstack.org/en/stable/yaml_configuration/
+
+# Resolver to choose a 'specific' stackage snapshot or a compiler version.
+# A snapshot resolver dictates the compiler version and the set of packages
+# to be used for project dependencies. For example:
+#
+# resolver: lts-3.5
+# resolver: nightly-2015-09-21
+# resolver: ghc-7.10.2
+# resolver: ghcjs-0.1.0_ghc-7.10.2
+# resolver:
+#  name: custom-snapshot
+#  location: "./custom-snapshot.yaml"
+resolver: lts-9.10
+
+# User packages to be built.
+# Various formats can be used as shown in the example below.
+#
+# packages:
+# - some-directory
+# - https://example.com/foo/bar/baz-0.0.2.tar.gz
+# - location:
+#    git: https://github.com/commercialhaskell/stack.git
+#    commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+# - location: https://github.com/commercialhaskell/stack/commit/e7b331f14bcffb8367cd58fbfc8b40ec7642100a
+#   extra-dep: true
+#  subdirs:
+#  - auto-update
+#  - wai
+#
+# A package marked 'extra-dep: true' will only be built if demanded by a
+# non-dependency (i.e. a user package), and its test suites and benchmarks
+# will not be run. This is useful for tweaking upstream packages.
+packages:
+- .
+# Dependency packages to be pulled from upstream that are not in the resolver
+# (e.g., acme-missiles-0.3)
+# extra-deps: []
+
+# Override default flag values for local packages and extra-deps
+# flags: {}
+
+# Extra package databases containing global packages
+# extra-package-dbs: []
+
+# Control whether we use the GHC we find on the path
+# system-ghc: true
+#
+# Require a specific version of stack, using version ranges
+# require-stack-version: -any # Default
+# require-stack-version: ">=1.5"
+#
+# Override the architecture used by stack, especially useful on Windows
+# arch: i386
+# arch: x86_64
+#
+# Extra directories used by stack for building
+# extra-include-dirs: [/path/to/dir]
+# extra-lib-dirs: [/path/to/dir]
+#
+# Allow a newer minor version of GHC than the snapshot specifies
+# compiler-check: newer-minor

test/Spec.hs

@@ -0,0 +1,2 @@
+main :: IO ()
+main = putStrLn "Test suite not yet implemented"