abt 0.1.0.0 → 0.1.0.1

raw patch · 9 files changed

+138/−105 lines, 9 filesdep +vinyldep −mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: vinyl

Dependencies removed: mtl

API changes (from Hackage documentation)

Files

• abt.cabal +4/−8
• src/Abt/Class/Abt.hs +17/−20
• src/Abt/Class/HEq1.hs +8/−0
• src/Abt/Class/Show1.hs +1/−1
• src/Abt/Concrete/LocallyNameless.hs +16/−11
• src/Abt/Tutorial.hs +76/−11
• src/Abt/Types.hs +0/−2
• src/Abt/Types/HList.hs +0/−43
• src/Abt/Types/View.hs +16/−9

@@ -1,15 +1,13 @@ name:                abt-version:             0.1.0.0+version:             0.1.0.1 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@@ -20,14 +18,12 @@                        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+                       vinyl >=0.5,+                       transformers+  ghc-options:         -Wall   hs-source-dirs:      src   default-language:    Haskell2010

@@ -10,28 +10,29 @@ ) 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 Control.Applicative hiding (Const)+import Data.Vinyl+import Data.Vinyl.Functor 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+-- nameless) term representaion, and a simple 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+class (Show1 o, Show v) ⇒ Abt (v ∷ *) (o ∷ [Nat] → *) (t ∷ Nat → *) | t → v o where   -- | Convert a 'View' into a term.   --   into     ∷ View v o n t     → t n -  -- | Convert a term into a first-order 'View'.+  -- | Convert a term into a simple 'View'.   --   out     ∷ MonadVar v m@@ -51,13 +52,13 @@     ∷ v     → t n     → t (S n)-  v \\ e = into $ (v :\ e)+  v \\ e = into $ v :\ e    -- | Construct an operator term.   --   ($$)     ∷ o ns-    → HList t ns+    → Rec t ns     → t Z   o $$ es = into $ o :$ es   infixl 1 $$@@ -74,12 +75,8 @@     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'+      v' :\ e'' → (v' \\) <$> subst e v e''+      o :$ es → (o $$) <$> subst e v `rtraverse` es    -- | Instantiate the bound variable of an abstraction.   --@@ -105,9 +102,9 @@       v :\ e' → do         L.delete v <$>           freeVars e'-      o :$ es → do-        concat <$>-          homogenizeA freeVars es+      _ :$ es →+        fmap concat . sequence . recordToList $+          Const . freeVars <<$>> es    -- | Render a term into a human-readable string.   --@@ -119,10 +116,10 @@     vu ← out e     case vu of       V v → return $ show v-      v :\ e → do-        e' ← toString e-        return $ show v ++ "." ++ e'+      v :\ e' → do+        estr ← toString e'+        return $ show v ++ "." ++ estr       o :$ es → do-        es' ← homogenizeA toString es+        es' ← sequence . recordToList $ Const . toString <<$>> es         return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]" 

@@ -1,11 +1,19 @@+{-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE UnicodeSyntax #-}  module Abt.Class.HEq1 where +import Data.Vinyl+ -- | 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++instance HEq1 el ⇒ HEq1 (Rec el) where+  RNil === RNil = True+  (x :& xs) === (y :& ys) = x === y && xs === ys+  _ === _ = False

@@ -8,7 +8,7 @@ -- class Show1 f where   showsPrec1 ∷ Int → f i → ShowS-  showsPrec1 i x = (show1 x ++)+  showsPrec1 _ x = (show1 x ++)    show1 ∷ f i → String   show1 x = showsPrec1 0 x ""

@@ -8,13 +8,13 @@  module Abt.Concrete.LocallyNameless ( Tm(..)+, Tm0 , Var(..) , varName , varIndex ) where  import Abt.Types.Nat-import Abt.Types.HList import Abt.Types.View import Abt.Class.HEq1 import Abt.Class.Show1@@ -22,6 +22,7 @@ import Abt.Class.Monad  import Control.Applicative+import Data.Vinyl  -- | A variable is a De Bruijn index, optionally decorated with a display name. data Var@@ -70,14 +71,18 @@   (\j' → Var n j')     <$> i j --- | Locally nameless terms with operators in @o@ at arity @n@.+-- | Locally nameless terms with operators in @o@ at order @n@. -- data Tm (o ∷ [Nat] → *) (n ∷ Nat) where-  Free ∷ Var → Tm o Z-  Bound ∷ Int → Tm o Z+  Free ∷ Var → Tm0 o+  Bound ∷ Int → Tm0 o   Abs ∷ Tm o n → Tm o (S n)-  App ∷ o ns → HList (Tm o) ns → Tm o Z+  App ∷ o ns → Rec (Tm o) ns → Tm0 o +-- | First order terms (i.e. terms not headed by abstractions).+--+type Tm0 o = Tm o Z+ instance HEq1 o ⇒ HEq1 (Tm o) where   Free v1 === Free v2 = v1 == v2   Bound m === Bound n = m == n@@ -93,8 +98,8 @@ 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+  Abs e → Abs $ shiftVar v (n + 1) e+  App p es → App p $ rmap (shiftVar v n) es  addVar   ∷ Var@@ -104,18 +109,18 @@ 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+  Abs e → Abs $ addVar v (n + 1) e+  App p es → App p $ rmap (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 :\ 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"+    Bound _ → fail "bound variable occured in out"     Abs e → do       v ← fresh       return $ v :\ addVar v 0 e

@@ -1,5 +1,6 @@-{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-}@@ -13,8 +14,9 @@ import Abt.Concrete.LocallyNameless  import Control.Applicative-import Control.Monad.Trans import Control.Monad.Trans.State.Strict+import Control.Monad.Trans.Maybe+import Data.Vinyl  -- | We'll start off with a monad in which to manipulate ABTs; we'll need some -- state for fresh variable generation.@@ -59,14 +61,77 @@   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.+-- | A monad transformer for small step operational semantics. ---example ∷ M [Var]-example = do+newtype StepT m α+  = StepT+  { runStepT ∷ MaybeT m α+  } deriving (Monad, Functor, Applicative, Alternative)++-- | To indicate that a term is in normal form.+--+stepsExhausted+  ∷ Applicative m+  ⇒ StepT m α+stepsExhausted = StepT . MaybeT $ pure Nothing++instance MonadVar Var m ⇒ MonadVar Var (StepT m) where+  fresh = StepT . MaybeT $ Just <$> fresh+  named str = StepT . MaybeT $ Just <$> named str++-- | A single evaluation step.+--+step+  ∷ Tm0 Lang+  → StepT M (Tm0 Lang)+step tm =+  out tm >>= \case+    Ap :$ m :& n :& RNil →+      out m >>= \case+        Lam :$ xe :& RNil → xe // n+        _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n+          where+            app a b = Ap $$ a :& b :& RNil+    _ → stepsExhausted++-- | The reflexive-transitive closure of a small-step operational semantics.+--+star+  ∷ Monad m+  ⇒ (α → StepT m α)+  → (α → m α)+star f a =+  runMaybeT (runStepT $ f a) >>=+    return a `maybe` star f++-- | Evaluate a term to normal form+--+eval ∷ Tm0 Lang → Tm0 Lang+eval = runM . star step++-- | @λx.x@+--+identityTm ∷ M (Tm0 Lang)+identityTm = do   x ← fresh-  y ← fresh-  let tm = Lam $$ x \\ (Ap $$ var x :* var y :* Nil) :* Nil-  freeVars tm+  return $ Lam $$ (x \\ var x) :& RNil++-- | @(λx.x)(λx.x)@+--+appTm ∷ M (Tm0 Lang)+appTm = do+  tm ← identityTm+  return $ Ap $$ tm :& tm :& RNil++-- | A demonstration of evaluating (and pretty-printing). Output:+--+-- @+-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@2.\@2]+-- @+--+main ∷ IO ()+main = do+  let mm = runM $ appTm >>= toString+      mm' = runM $ appTm >>= toString . eval+  print $ mm ++ " ~>* " ++ mm'+

@@ -2,10 +2,8 @@ -- 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

@@ -1,43 +0,0 @@-{-# 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-

@@ -7,29 +7,36 @@  module Abt.Types.View ( View(..)+, View0 , mapView ) where  import Abt.Types.Nat-import Abt.Types.HList+import Data.Vinyl  -- | @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.+-- by arities; @n@ is the "higher type"/order 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 ∷ v → View0 v o φ   (:\) ∷ v → φ n → View v o (S n) φ-  (:$) ∷ o ns → HList φ ns → View v o Z φ+  (:$) ∷ o ns → Rec φ ns → View0 v o φ +infixl 2 :$++-- | First order term views.+--+type View0 v o φ = 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+mapView η = \case   V v → V v-  v :\ e → v :\ eta e-  o :$ es → o :$ hmap eta es+  v :\ e → v :\ η e+  o :$ es → o :$ rmap η es