packages feed

nom 0.1.0.1 → 0.1.0.2

raw patch · 11 files changed

+172/−52 lines, 11 files

Files

CHANGELOG.markdown view
@@ -1,3 +1,7 @@+0.1.0.2+---+GHC 8.8.3 -> GHC 8.10.1+ 0.1.0.1 --- Fixed build error with Haddock documentation (missing file)
nom.cabal view
@@ -1,6 +1,6 @@ cabal-version:      2.0 name:               nom-version:            0.1.0.1+version:            0.1.0.2 description:        Nominal-flavoured implementation of data in a context of local names, following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).                     __The recommended landing page is "Language.Nominal", so please go there first.__ See also: a tutorial in "Language.Nominal.Examples.Tutorial"; a short development of untyped lambda-calculus in "Language.Nominal.Examples.UntypedLambda"; an example development of System F in "Language.Nominal.Examples.SystemF"; and an example development of an EUTxO-style blockchain in "Language.Nominal.Examples.IdealisedEUTxO". homepage:           https://github.com/bellissimogiorno/nominal#readme@@ -44,6 +44,7 @@       Language.Nominal.Unique       Language.Nominal.Equivar       Language.Nominal.Examples.SystemF+      Language.Nominal.Examples.Graph       Language.Nominal.Examples.IdealisedEUTxO       Language.Nominal.Examples.UntypedLambda       Language.Nominal.Examples.Assembly1
src/Language/Nominal.hs view
@@ -92,7 +92,7 @@ /Note:/ "having empty support" does /not/ mean "having no atoms".  It means "symmetric under swapping atoms", which is not at all the same idea.  * 'Language.Nominal.Name.Nameless': types like @Int@, @String@, and @()@ that are guaranteed atoms-free.  * 'Language.Nominal.Nom.KNom' and 'Language.Nominal.Nom.Nom': An atoms-binding monad.-* 'Language.Nominal.Nom.Binder': A typeclass for functions acting on binding types.+* 'Language.Nominal.Binder.Binder': A typeclass for functions acting on binding types. * 'Language.Nominal.Abs.KAbs' and 'Language.Nominal.Abs.Abs': A name-abstracting functor. * 'Language.Nominal.Name.KRestrict' and 'Language.Nominal.Name.Restrict': A typeclass of types with an inherent notion of atoms-binding. * 'Language.Nominal.Unify.KUnifyPerm' and 'Language.Nominal.Unify.UnifyPerm': Typeclasses of types with a notion of unification by injective partial functions on atoms.
+ src/Language/Nominal/Examples/Graph.hs view
@@ -0,0 +1,84 @@+{-|+Module      : Algebraic graphs with binding +Description : Extending algebraic graphs with nominal-style binding +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++A development file to build on <https://hackage.haskell.org/package/algebraic-graphs Andrey Mokhov's algebraic-graphs> library.+__THIS FILE IS UNDER DEVELOPMENT__+Connect should be implemented such that only /free/ vertices are connected; not bound ones.  Overlay should be capture-avoiding (which should be automatic). +-}++{-# LANGUAGE InstanceSigs          +           , DeriveGeneric         +           , FlexibleContexts +           , LambdaCase +           , MultiParamTypeClasses +           , DeriveAnyClass       -- to derive 'Swappable' +           , DeriveDataTypeable   -- to derive 'Data' +           , FlexibleInstances     +           , TypeOperators        -- to use :. in instances+#-}+++module Language.Nominal.Examples.Graph+    where++import GHC.Generics+-- import Data.Generics     hiding (Generic, typeOf)+-- import Algebra.Graph.HigherKinded.Class +-- import Control.Compose -- for :.+-- import Data.Function    ((&))++import Language.Nominal.Name +import Language.Nominal.NameSet +import Language.Nominal.Nom++-- | A datatype of graphs with binding.  +-- Perhaps should parameterise over atom type (see 'KAtom').  For now, I use the default atom type 'Tom'.+data Graph a = Empty+             | Vertex a+             | Overlay (Graph a) (Graph a)+             | Connect (Graph a) (Graph a)+             | Restrict (Nom (Graph a))+             deriving (Show, Generic, Swappable)++-- | Restriction action just passes the restriction on to the deep embedding+instance Swappable a => KRestrict Tom (Graph a) where+   restrict atms g = Restrict (res atms g)++-- | Fold on graphs with binding.  +-- Just like fold on graphs, but with an extra restriction operation, which we go under in a capture-avoiding manner. +foldg :: b -> (a -> b) -> (b -> b -> b) -> (b -> b -> b) -> (Nom b -> b) -> Graph a -> b+foldg e v o c r = go+  where+    go Empty         = e+    go (Vertex  x  ) = v x+    go (Overlay x y) = o (go x) (go y)+    go (Connect x y) = c (go x) (go y)+    go (Restrict x') = r (go <$> x') -- special operators, like @@! and @@., are available to construct @r@. +{-# INLINE [0] foldg #-}++-- | Filter a list of vertices to obtain those vertices for which @atms :: ['Atom']@ is fresh +filterApart :: Support a => [Atom] -> [a] -> [a]+filterApart atms = filter $ apart atms++{- instance Graph g => Graph ((KNom s) :. g) where+   connect :: (KNom s :. g) a -> (KNom s :. g) a -> (KNom s :. g) a+   connect g1' g2' = O $ (unO g1') @@. \gas1 g1 -> (unO g2') @@. \gas2 g2 ->+      let h1 = filter (kapart (Proxy :: Proxy s) gas1) (vertices g1) +          h2 = filter (kapart (Proxy :: Proxy s) gas2) (vertices g2) +      in+          res $ g1 <|> g2 <|> (biclique h1 h2)+-}+   +{-+   connect g1' g2' = O $ (genUnNom' . unO $ g1') & \(gas1, g1) -> (genUnNom' . unO $ g2') & \(gas2, g2) ->+      let h1 = filter (kapart gas1) (vertices g1) +          h2 = filter (kapart gas2) (vertices g2) +      in+          res $ g1 <|> g2 <|> (biclique h1 h2)+-}
src/Language/Nominal/Examples/UntypedLambda.hs view
@@ -47,7 +47,7 @@ data Exp = V Var              -- ^ Variable           | Exp :@ Exp         -- ^ Application           | Lam (KAbs Var Exp) -- ^ Lambda, using abstraction-type - deriving (Eq, Generic, Data, Swappable, Show)+ deriving (Eq, Generic, Data, Swappable) -- , Show)  -- | helper for building lambda-abstractions  lam :: Var -> Exp -> Exp @@ -77,14 +77,12 @@  -- | weak head normal form of a lambda-term. whnf :: Exp -> Exp -whnf (f :@ a) = case whnf f of-  Lam b' -> whnf $ b' `conc` a  -  f'     -> f' :@ a-whnf e = e+whnf (Lam b' :@ a) = whnf $ b' `conc` a  +whnf             e = e  -- | (\x x) y example1 :: Exp-example1 = (\[x, y] -> lam x $ V x :@ V y) `genAppC` freshNames ["x", "y"] +example1 = (\[x, y] -> lam x (V x) :@ V y) `genAppC` freshNames ["x", "y"]  -- | y example1whnf :: Exp example1whnf = whnf example1@@ -96,3 +94,8 @@ example2whnf :: Exp example2whnf = whnf example2 +instance Show Exp where+   show     (V v) = show v +   show   (Lam e) = "(λ" ++ (show e) ++ ")"+   show (e :@ e') = (show e) ++ " " ++ (show e')+
src/Language/Nominal/Name.hs view
@@ -291,7 +291,7 @@ kswpN :: (Typeable s, Swappable a) => KName s t -> KName s t -> a -> a kswpN n n' = kswp (nameAtom n) (nameAtom n')  --- | A name swap for a @'Tom'@-name.  Discards the names' labels and calls a @'Tom'@-atom swapping.+-- | A name swap for a @'Tom'@-name.  Discards the names' labels and calls a @'Tom'@-swapping. swpN :: Swappable a => Name t -> Name t -> a -> a swpN = kswpN  @@ -314,26 +314,28 @@  deriving via Nameless Bool instance Swappable Bool deriving via Nameless Int  instance Swappable Int+deriving via Nameless Integer instance Swappable Integer deriving via Nameless ()   instance Swappable () deriving via Nameless Char instance Swappable Char - -- * Generics support for @'KSwappable'@  class GSwappable f where     gswp :: Typeable s => KAtom s -> KAtom s -> f x -> f x +-- Distributes through datatype-formers+instance (GSwappable f, GSwappable g) => GSwappable ((:*:) f g) where  -- products+    gswp m n (x :*: y) = gswp m n x :*: gswp m n y+-- Action on a leaf is trivial+instance GSwappable U1 where   -- one constructor, no arguments+    gswp _ _ U1 = U1+ instance GSwappable V1 where   -- empty types, no instances     gswp _ _ x = case x of -instance GSwappable U1 where   -- one constructor, no arguments-    gswp _ _ U1 = U1  instance Swappable c => GSwappable (K1 i c) where  -- base case.  wrapper for all of some type c so we escape back out to swp.       gswp m n x = K1 $ kswp m n $ unK1 x--instance (GSwappable f, GSwappable g) => GSwappable ((:*:) f g) where  -- products-    gswp m n (x :*: y) = gswp m n x :*: gswp m n y  instance (GSwappable f, GSwappable g) => GSwappable ((:+:) f g) where  -- sums     gswp m n (L1 x) = L1 $ gswp m n x
src/Language/Nominal/NameSet.hs view
@@ -89,6 +89,7 @@ deriving via Nameless Bool instance Typeable s => KSupport s Bool deriving via Nameless Char instance Typeable s => KSupport s Char deriving via Nameless Int  instance Typeable s => KSupport s Int+deriving via Nameless Integer instance Typeable s => KSupport s Integer  -- order: nameless, tuple, list, nonempty list, maybe, sum, atom, name, nom, abs  instance (Typeable s, Typeable t) => KSupport s (KAtom t) where  @@ -156,7 +157,8 @@  -- | Form of restriction that takes names instead of atoms.  Just discards name labels and calls @'restrict'@. restrictN :: KRestrict s a => [KName s t] -> a -> a-restrictN l = restrict (nameAtom <$> l)+restrictN = restrict . (fmap nameAtom) +-- restrictN l = restrict (nameAtom <$> l)   -- | Restriction is trivial on elements of nameless types @@ -187,20 +189,21 @@ class GSupport s f where     gsupp :: f x -> Set (KAtom s) -instance GSupport s V1 where-    gsupp x = case x of-+-- | Support distributes through datatype-formers, taking unions+instance (GSupport s f, GSupport s g) => GSupport s (f :*: g) where+    gsupp (x :*: y) = gsupp x `S.union` gsupp y+-- | Leaf has empty support instance GSupport s U1 where     gsupp U1 = S.empty +instance GSupport s V1 where+    gsupp x = case x of+ instance GSupport s f => GSupport s (M1 i t f) where     gsupp = gsupp . unM1  instance KSupport s c => GSupport s (K1 i c) where     gsupp = ksupp Proxy . unK1--instance (GSupport s f, GSupport s g) => GSupport s (f :*: g) where-    gsupp (x :*: y) = gsupp x `S.union` gsupp y  instance (GSupport s f, GSupport s g) => GSupport s (f :+: g) where     gsupp (L1 x) = gsupp x
src/Language/Nominal/Nom.hs view
@@ -46,7 +46,9 @@      -- * Destroying a @'Nom'@      , unNom, nomToIO      -- * Creating fresh ids in a @'Nom'@-     , freshKAtom, freshAtom, freshKAtoms, freshAtoms, freshKName, freshName, freshKNames, freshNames -- , atFresh+     , freshKAtom, freshAtom, freshKAtoms, freshAtoms +     , freshKName, freshName, freshKNames, freshNames +     , freshKNameIO, freshNameIO, freshKNamesIO, freshNamesIO       -- * 'KNom' and other functors      -- $functor      , transposeNomF @@ -189,7 +191,7 @@ -- * Creating fresh ids in a @'Nom'@  -- | Create a fresh atom-in-nominal-context-freshKAtom :: Typeable s => KNom s (KAtom s)+freshKAtom :: KNom s (KAtom s) freshKAtom = Nom $ do -- IO monad    [a] <- freshKAtomsIO [()]    return $ enter [a] a@@ -199,7 +201,7 @@ freshAtom = freshKAtom  -- | Fresh @'Traversable' m@ of atoms (e.g. @m@ is list or stream)-freshKAtoms :: (Traversable m, Typeable s) => m t -> KNom s (m (KAtom s))+freshKAtoms :: Traversable m => m t -> KNom s (m (KAtom s)) freshKAtoms = mapM (const freshKAtom)  -- | Fresh @'Traversable' m@ of atoms (e.g. @m@ is list or stream).@@ -207,12 +209,13 @@ freshAtoms :: Traversable m => m t -> Nom (m Atom) freshAtoms = freshKAtoms + -- | Create a fresh name-in-a-nominal-context with label @t@-freshKName :: Typeable s => t -> KNom s (KName s t)+freshKName :: t -> KNom s (KName s t) freshKName t = freshKAtom <&> Name t  -- | Create fresh names-in-a-nominal-context-freshKNames :: (Traversable m, Typeable s) => m t -> KNom s (m (KName s t))+freshKNames :: Traversable m => m t -> KNom s (m (KName s t)) freshKNames = mapM freshKName  -- | Canonical version of 'freshKName' for @'Tom'@ name.@@ -223,6 +226,24 @@ freshNames :: Traversable m => m t -> Nom (m (Name t)) freshNames = freshKNames ++-- | Create a fresh name-in-a-nominal-context with label @t@+freshKNameIO :: t -> IO (KName s t)+freshKNameIO = nomToIO . freshKName  ++-- | Create fresh names-in-a-nominal-context+freshKNamesIO :: Traversable m => m t -> IO (m (KName s t))+freshKNamesIO = nomToIO . freshKNames++-- | Canonical version of 'freshKName' for @'Tom'@ name.+freshNameIO :: t -> IO (Name t)+freshNameIO = nomToIO . freshKName++-- | Canonical version of 'freshKNames' for @'Tom'@ names.+freshNamesIO :: Traversable m => m t -> IO (m (Name t))+freshNamesIO = nomToIO . freshKNames++ {--  -- | atFresh f returns the value of f at a fresh name with label @t@ atFresh :: Typeable s => t -> (KName s t -> a) -> KNom s a@@ -239,11 +260,10 @@ * 'transposeMF' * 'transposeFM' -Taken together, these functions are making a point that 'KNom' is compatible with your favourite container type.  Because 'KNom' can commuted, there is no need to wonder whether (for example) a graph-with-binding should be a graph with binding on the vertices, or on the edges, or on the graph overall, or any combination.  All of these are valid design decisions and one may be more /convenient/ than the other, but in the end we can isomorphically commute to a single top-level 'KNom' binding.+Taken together, these functions are making a point that 'KNom' is compatible with your favourite container type.  Because 'KNom' commutes, there is no need to wonder whether (for example) a graph-with-binding should be a graph with binding on the vertices, or on the edges, or on the graph overall, or any combination.  All of these are valid design decisions and one may be more /convenient/ than the other, but we know we can isomorphically commute to a single top-level 'KNom' binding.  In that sense, 'KNom' captures a general theory of binding.-It is also a mathematical justification for why the 'Language.Nominal.Binder.Binder' typeclass turns out to be so useful.-+This also mathematically justifies why the 'Language.Nominal.Binder.Binder' typeclass is so useful. -}
src/Language/Nominal/Sub.hs view
@@ -67,10 +67,11 @@ instance KSub n x (Nameless a) where    sub _ _ = id -deriving via Nameless Bool instance KSub n x Bool-deriving via Nameless Int  instance KSub n x Int deriving via Nameless ()   instance KSub n x ()+deriving via Nameless Bool instance KSub n x Bool deriving via Nameless Char instance KSub n x Char+deriving via Nameless Int  instance KSub n x Int+deriving via Nameless Integer instance KSub n x Integer  instance (KSub n x a, KSub n x b) => KSub n x (a, b) instance (KSub n x a, KSub n x b, KSub n x c) => KSub n x (a, b, c)@@ -109,20 +110,21 @@ class GSub n x f where     gsub :: n -> x -> f w -> f w  -instance GSub n x V1 where-    gsub _ _ y = case y of-+-- | Distributes through datatype-formers+instance (GSub n x f, GSub n x g) => GSub n x (f :*: g) where+    gsub n x (y :*: z) = gsub n x y :*: gsub n x z+-- | Action on a leaf is trivial instance GSub n x U1 where     gsub _ _ = id +instance GSub n x V1 where+    gsub _ _ y = case y of+ instance GSub n x f => GSub n x (M1 i t f) where     gsub n x = M1 . gsub n x . unM1  instance KSub n x c => GSub n x (K1 i c) where     gsub n x = K1 . sub n x . unK1--instance (GSub n x f, GSub n x g) => GSub n x (f :*: g) where-    gsub n x (y :*: z) = gsub n x y :*: gsub n x z  instance (GSub n x f, GSub n x g) => GSub n x (f :+: g) where     gsub n x (L1 y) = L1 $ gsub n x y
src/Language/Nominal/Unify.hs view
@@ -255,10 +255,11 @@         | otherwise = Ren Nothing     ren _ = id -deriving via Nameless Bool instance Typeable s => KUnifyPerm s Bool-deriving via Nameless Int  instance Typeable s => KUnifyPerm s Int deriving via Nameless ()   instance Typeable s => KUnifyPerm s ()+deriving via Nameless Bool instance Typeable s => KUnifyPerm s Bool deriving via Nameless Char instance Typeable s => KUnifyPerm s Char+deriving via Nameless Int  instance Typeable s => KUnifyPerm s Int+deriving via Nameless Integer instance Typeable s => KUnifyPerm s Integer  instance (KUnifyPerm s a, KUnifyPerm s b) => KUnifyPerm s (a, b) instance (KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c) => KUnifyPerm s (a, b, c)@@ -330,17 +331,19 @@     gunifyPerm :: f x -> f x -> KRen s     gren       :: KRen s -> f x -> f x -instance GUnifyPerm s V1 where-    gunifyPerm x = case x of-    gren _ x = case x of+-- Unifiers accumulate on datatype-formers+instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :*: g) where+    gunifyPerm (x1 :*: y1) (x2 :*: y2) = gunifyPerm x1 x2 <> gunifyPerm y1 y2+    gren r (x :*: y) = gren r x :*: gren r y +-- Unifier on a leaf is trivial instance GUnifyPerm s U1 where     gunifyPerm U1 U1 = mempty     gren _ U1 = U1 -instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :*: g) where-    gunifyPerm (x1 :*: y1) (x2 :*: y2) = gunifyPerm x1 x2 <> gunifyPerm y1 y2-    gren r (x :*: y) = gren r x :*: gren r y+instance GUnifyPerm s V1 where+    gunifyPerm x = case x of+    gren _ x = case x of  instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :+: g) where
stack.yaml view
@@ -1,9 +1,7 @@-resolver: lts-15.8+resolver: nightly-2020-07-14 packages: - . extra-deps:- - Unique-0.4.7.7@sha256:2269d3528271e25d34542e7c24a4e541e27ec33460e1ea00845da95b82eec6fa,2777- - algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129- - extra-1.6.21- - finite-typelits-0.1.4.2  # for Data.Finite in IdealisedEUTxOSpec- - data-default-0.7.1.1     # for Data.Default+- Unique-0.4.7.7@sha256:2269d3528271e25d34542e7c24a4e541e27ec33460e1ea00845da95b82eec6fa,2777+- algebra-4.3.1@sha256:323cf20c508e0b71422b767ff3a89e4188f68aa59b2df9d0fe6e9f9bae7938fb,4129+- extra-1.6.21@sha256:1e04429779702160356af6b3b8dd8531d5997f69bb1419f80a1a33b690c92f25,2757