packages feed

abt (empty) → 0.1.0.0

raw patch · 14 files changed

+527/−0 lines, 14 filesdep +basedep +mtldep +transformerssetup-changed

Dependencies added: base, mtl, transformers

Files

+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2014 Jonathan Sterling++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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ abt.cabal view
@@ -0,0 +1,33 @@+name:                abt+version:             0.1.0.0+synopsis:            Abstract binding trees for Haskell+description:         A Haskell port of the Carnegie Mellon ABT library (SML), with some improvements.+license:             MIT+license-file:        LICENSE+author:              Jonathan Sterling+maintainer:          jon@jonmsterling.com+-- copyright:+category:            Language+build-type:          Simple+-- extra-source-files:+cabal-version:       >=1.10++library+  exposed-modules:     Abt.Class,+                       Abt.Class.Show1,+                       Abt.Class.HEq1,+                       Abt.Class.Monad,+                       Abt.Class.Abt,+                       Abt.Types,+                       Abt.Types.Nat,+                       Abt.Types.HList,+                       Abt.Types.View,+                       Abt.Concrete.LocallyNameless+                       Abt.Tutorial+  -- other-modules:+  -- other-extensions:+  build-depends:       base >=4.7 && <4.8,+                       transformers,+                       mtl+  hs-source-dirs:      src+  default-language:    Haskell2010
+ src/Abt/Class.hs view
@@ -0,0 +1,15 @@+-- | The core signatures used to define abstract binding trees.+--+module Abt.Class+( module Abt.Class.Abt+, module Abt.Class.Monad+, module Abt.Class.Show1+, module Abt.Class.HEq1+) where++import Abt.Class.Abt+import Abt.Class.Monad+import Abt.Class.Show1+import Abt.Class.HEq1++
+ src/Abt/Class/Abt.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Class.Abt+( Abt(..)+) where++import Abt.Types.Nat+import Abt.Types.HList+import Abt.Types.View+import Abt.Class.Monad+import Abt.Class.Show1++import Control.Applicative+import qualified Data.List as L++-- | The 'Abt' signature represents mediation between an arbitrary (possibly+-- nameless) term representaion, and a first-order one (the 'View'). Based on+-- the (effectful) ismorphism @'into' / 'out'@ between representations, many+-- operations can be defined generically for arbitrary operator sets, including+-- substitution and aggregation of free variables.+--+class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o, o → t where+  -- | Convert a 'View' into a term.+  --+  into+    ∷ View v o n t+    → t n++  -- | Convert a term into a first-order 'View'.+  --+  out+    ∷ MonadVar v m+    ⇒ t n+    → m (View v o n t)++  -- | The injection from variables to terms.+  --+  var+    ∷ v+    → t Z+  var = into . V++  -- | Construct an abstraction.+  --+  (\\)+    ∷ v+    → t n+    → t (S n)+  v \\ e = into $ (v :\ e)++  -- | Construct an operator term.+  --+  ($$)+    ∷ o ns+    → HList t ns+    → t Z+  o $$ es = into $ o :$ es+  infixl 1 $$++  -- | Substitute a term for a variable.+  --+  subst+    ∷ MonadVar v m+    ⇒ t Z+    → v+    → t n+    → m (t n)+  subst e v e' = do+    oe' ← out e'+    case oe' of+      V v' → return $ if v == v' then e else e'+      v' :\ e'' → do+        e''' ← subst e v e''+        return $ v' \\ e'''+      o :$ es → do+        es' ← htraverse (subst e v) es+        return $ o $$ es'++  -- | Instantiate the bound variable of an abstraction.+  --+  (//)+    ∷ MonadVar v m+    ⇒ t (S n)+    → t Z+    → m (t n)+  xe // e' = do+    v :\ e ← out xe+    subst e' v e++  -- | Compute the free variables of a term.+  --+  freeVars+    ∷ MonadVar v m+    ⇒ t n+    → m [v]+  freeVars e = do+    oe ← out e+    case oe of+      V v → return [v]+      v :\ e' → do+        L.delete v <$>+          freeVars e'+      o :$ es → do+        concat <$>+          homogenizeA freeVars es++  -- | Render a term into a human-readable string.+  --+  toString+    ∷ MonadVar v m+    ⇒ t n+    → m String+  toString e = do+    vu ← out e+    case vu of+      V v → return $ show v+      v :\ e → do+        e' ← toString e+        return $ show v ++ "." ++ e'+      o :$ es → do+        es' ← homogenizeA toString es+        return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"+
+ src/Abt/Class/HEq1.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Class.HEq1 where++-- | Uniform variant of 'Eq' for indexed types. This is different from+-- 'Data.Functor.Eq1' in that it is properly kind polymorphic and crucially+-- heterogeneous, and it places no constraint on the index.+--+class HEq1 f where+  (===) ∷ f i → f j → Bool
+ src/Abt/Class/Monad.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Class.Monad where++import Control.Applicative++class (Ord v, Eq v, Show v, Monad m, Applicative m) ⇒ MonadVar v m | m → v where+  -- | Generates a fresh variable+  fresh ∷ m v++  -- | Generates a fresh variable tagged with a name+  named ∷ String → m v
+ src/Abt/Class/Show1.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Class.Show1 where++-- | Uniform variant of 'Show' for indexed types. This is different from+-- 'Data.Functor.Show1' in that it is properly kind polymorphic.+--+class Show1 f where+  showsPrec1 ∷ Int → f i → ShowS+  showsPrec1 i x = (show1 x ++)++  show1 ∷ f i → String+  show1 x = showsPrec1 0 x ""+
+ src/Abt/Concrete/LocallyNameless.hs view
@@ -0,0 +1,122 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Concrete.LocallyNameless+( Tm(..)+, Var(..)+, varName+, varIndex+) where++import Abt.Types.Nat+import Abt.Types.HList+import Abt.Types.View+import Abt.Class.HEq1+import Abt.Class.Show1+import Abt.Class.Abt+import Abt.Class.Monad++import Control.Applicative++-- | A variable is a De Bruijn index, optionally decorated with a display name.+data Var+  = Var+  { _varName ∷ !(Maybe String)+  , _varIndex ∷ !Int+  }++instance Show Var where+  show (Var (Just v) _) = v+  show (Var Nothing i) = "@" ++ show i++instance Eq Var where+  (Var _ i) == (Var _ j) = i == j++instance Ord Var where+  compare (Var _ i) (Var _ j) = compare i j++-- | A lens for '_varName'.+--+-- @+-- varName ∷ Lens' 'Var' ('Maybe' 'String')+-- @+--+varName+  ∷ Functor f+  ⇒ (Maybe String → f (Maybe String))+  → Var+  → f Var+varName i (Var n j) =+  (\n' → Var n' j)+    <$> i n++-- | A lens for '_varIndex'.+--+-- @+-- varIndex ∷ Lens' 'Var' 'Int'+-- @+--+varIndex+  ∷ Functor f+  ⇒ (Int → f Int)+  → Var+  → f Var+varIndex i (Var n j) =+  (\j' → Var n j')+    <$> i j++-- | Locally nameless terms with operators in @o@ at arity @n@.+--+data Tm (o ∷ [Nat] → *) (n ∷ Nat) where+  Free ∷ Var → Tm o Z+  Bound ∷ Int → Tm o Z+  Abs ∷ Tm o n → Tm o (S n)+  App ∷ o ns → HList (Tm o) ns → Tm o Z++instance HEq1 o ⇒ HEq1 (Tm o) where+  Free v1 === Free v2 = v1 == v2+  Bound m === Bound n = m == n+  Abs e1 === Abs e2 = e1 === e2+  App o1 es1 === App o2 es2 = o1 === o2 && es1 === es2+  _ === _ = False++shiftVar+  ∷ Var+  → Int+  → Tm o n+  → Tm o n+shiftVar v n = \case+  Free v' → if v == v' then Bound n else Free v'+  Bound m → Bound m+  Abs e → Abs (shiftVar v (n + 1) e)+  App p es → App p $ hmap (shiftVar v n) es++addVar+  ∷ Var+  → Int+  → Tm o n+  → Tm o n+addVar v n = \case+  Free v' → Free v'+  Bound m → if m == n then Free v else Bound m+  Abs e → Abs (addVar v (n + 1) e)+  App p es → App p $ hmap (addVar v n) es++instance Show1 o ⇒ Abt Var o (Tm o) where+  into = \case+    V v → Free v+    v :\ e → Abs (shiftVar v 0 e)+    v :$ es → App v es++  out = \case+    Free v → return $ V v+    Bound n → fail "bound variable occured in out"+    Abs e → do+      v ← fresh+      return $ v :\ addVar v 0 e+    App p es → return $ p :$ es
+ src/Abt/Tutorial.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Tutorial where++import Abt.Class+import Abt.Types+import Abt.Concrete.LocallyNameless++import Control.Applicative+import Control.Monad.Trans+import Control.Monad.Trans.State.Strict++-- | We'll start off with a monad in which to manipulate ABTs; we'll need some+-- state for fresh variable generation.+--+newtype M α+  = M+  { _M ∷ State Int α+  } deriving (Functor, Applicative, Monad)++-- | We'll run an ABT computation by starting the variable counter at @0@.+--+runM ∷ M α → α+runM (M m) = evalState m 0++-- | Check out the source to see fresh variable generation.+--+instance MonadVar Var M where+  fresh = M $ do+    n ← get+    let n' = n + 1+    put n'+    return $ Var Nothing n'++  named a = do+    v ← fresh+    return $ v { _varName = Just a }++-- | Next, we'll define the operators for a tiny lambda calculus as a datatype+-- indexed by arities.+--+data Lang ns where+  Lam ∷ Lang '[S Z]+  Ap ∷ Lang '[Z,Z]++instance Show1 Lang where+  show1 = \case+    Lam → "lam"+    Ap → "ap"++instance HEq1 Lang where+  Lam === Lam = True+  Ap === Ap = True+  _ === _ = False++-- | Check out the source to see this example term: note that number of+-- arguments and presence of abstractions is guaranteed by the types.  The+-- representation is not scope-safe (i.e. free variables are permitted), but+-- that's how we want it.+--+example ∷ M [Var]+example = do+  x ← fresh+  y ← fresh+  let tm = Lam $$ x \\ (Ap $$ var x :* var y :* Nil) :* Nil+  freeVars tm
+ src/Abt/Types.hs view
@@ -0,0 +1,11 @@+-- | The core structures used to define the Abt signatures.+--+module Abt.Types+( module Abt.Types.Nat+, module Abt.Types.HList+, module Abt.Types.View+) where++import Abt.Types.Nat+import Abt.Types.HList+import Abt.Types.View
+ src/Abt/Types/HList.hs view
@@ -0,0 +1,43 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Types.HList+( HList(..)+, hmap+, htraverse+, homogenizeA+) where++import Control.Applicative+import Abt.Class.HEq1++data HList ∷ (κ → *) → [κ] → * where+  Nil ∷ HList el '[]+  (:*) ∷ el x → HList el xs → HList el (x ': xs)+infixr 8 :*++hmap ∷ (∀ x. f x → g x) → HList f xs → HList g xs+hmap η = \case+  Nil → Nil+  x :* xs → η x :* hmap η xs++htraverse ∷ Applicative h ⇒ (∀ x. f x → h (g x)) → HList f xs → h (HList g xs)+htraverse η = \case+  Nil → pure Nil+  x :* xs → (:*) <$> η x <*> htraverse η xs++homogenizeA ∷ Applicative h ⇒ (∀ x. el x → h α) → HList el xs → h [α]+homogenizeA η = \case+  Nil → pure []+  x :* xs → (:) <$> η x <*> homogenizeA η xs++instance HEq1 el ⇒ HEq1 (HList el) where+  Nil === Nil = True+  (x :* xs) === (y :* ys) = x === y && xs === ys+  _ === _ = False+
+ src/Abt/Types/Nat.hs view
@@ -0,0 +1,6 @@+module Abt.Types.Nat where++data Nat+  = Z+  | S !Nat+
+ src/Abt/Types/View.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE UnicodeSyntax #-}++module Abt.Types.View+( View(..)+, mapView+) where++import Abt.Types.Nat+import Abt.Types.HList++-- | @v@ is the type of variables; @o@ is the type of operators parameterized+-- by arities; @n@ is the "higher type" of the term (i.e. a term has @n=0@, a+-- single binding has @n=1@, etc.); @φ@ is the functor which interprets the+-- inner structure of the view.+--+data View (v ∷ *) (o ∷ [Nat] → *) (n ∷ Nat) (φ ∷ Nat → *) where+  V ∷ v → View v o Z φ+  (:\) ∷ v → φ n → View v o (S n) φ+  (:$) ∷ o ns → HList φ ns → View v o Z φ++-- | Views are a (higher) functor.+--+mapView+  ∷ (∀ j. φ j → ψ j) -- ^ a natural transformation @φ → ψ@+  → View v o n φ -- ^ a view at @φ@+  → View v o n ψ+mapView eta = \case+  V v → V v+  v :\ e → v :\ eta e+  o :$ es → o :$ hmap eta es