packages feed

abt 0.1.0.1 → 0.1.0.2

raw patch · 6 files changed

+192/−33 lines, 6 filesdep +profunctors

Dependencies added: profunctors

Files

abt.cabal view
@@ -1,5 +1,5 @@ name:                abt-version:             0.1.0.1+version:             0.1.0.2 synopsis:            Abstract binding trees for Haskell description:         A Haskell port of the Carnegie Mellon ABT library (SML), with some improvements. license:             MIT@@ -23,6 +23,7 @@                        Abt.Tutorial   build-depends:       base >=4.7 && <4.8,                        vinyl >=0.5,+                       profunctors >=4.3.2,                        transformers   ghc-options:         -Wall   hs-source-dirs:      src
src/Abt/Class/Abt.hs view
@@ -99,7 +99,7 @@     oe ← out e     case oe of       V v → return [v]-      v :\ e' → do+      v :\ e' →         L.delete v <$>           freeVars e'       _ :$ es →@@ -119,6 +119,7 @@       v :\ e' → do         estr ← toString e'         return $ show v ++ "." ++ estr+      o :$ RNil → return $ show1 o       o :$ es → do         es' ← sequence . recordToList $ Const . toString <<$>> es         return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"
src/Abt/Class/HEq1.hs view
@@ -1,19 +1,42 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UnicodeSyntax #-}  module Abt.Class.HEq1 where +import Control.Applicative import Data.Vinyl +-- | Essentially, Martin-Löf's identity type.+--+data a :=: b where+  Refl ∷ a :=: a++-- | Type constructors are extensional.+--+cong ∷ a :=: b → f a :=: f b+cong Refl = Refl+ -- | 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.+-- heterogeneous, and it places no constraint on the index. Because it is+-- heterogeneous, it is useful to project equality in the base space from+-- equality in the total space. -- class HEq1 f where+  -- | When both sides are equal, give in addition a proof that their indices+  -- are equal; otherwise return 'Nothing'.+  --+  heq1 ∷ f i → f j → Maybe (i :=: j)++  -- | A boolean version of 'heq1', which must agree with it.+  --   (===) ∷ f i → f j → Bool+  x === y = maybe False (const True) $ heq1 x y  instance HEq1 el ⇒ HEq1 (Rec el) where-  RNil === RNil = True-  (x :& xs) === (y :& ys) = x === y && xs === ys-  _ === _ = False+  heq1 RNil RNil = Just Refl+  heq1 (x :& xs) (y :& ys)+    | Just Refl ← heq1 x y = cong <$> heq1 xs ys+  heq1 _ _ = Nothing
src/Abt/Concrete/LocallyNameless.hs view
@@ -9,6 +9,7 @@ module Abt.Concrete.LocallyNameless ( Tm(..) , Tm0+, _TmOp , Var(..) , varName , varIndex@@ -22,6 +23,7 @@ import Abt.Class.Monad  import Control.Applicative+import Data.Profunctor import Data.Vinyl  -- | A variable is a De Bruijn index, optionally decorated with a display name.@@ -44,7 +46,7 @@ -- | A lens for '_varName'. -- -- @--- varName ∷ Lens' 'Var' ('Maybe' 'String')+-- 'varName' ∷ Lens' 'Var' ('Maybe' 'String') -- @ -- varName@@ -59,7 +61,7 @@ -- | A lens for '_varIndex'. -- -- @--- varIndex ∷ Lens' 'Var' 'Int'+-- 'varIndex' ∷ Lens' 'Var' 'Int' -- @ -- varIndex@@ -84,11 +86,13 @@ 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-  Abs e1 === Abs e2 = e1 === e2-  App o1 es1 === App o2 es2 = o1 === o2 && es1 === es2-  _ === _ = False+  heq1 (Free v1) (Free v2) | v1 == v2 = Just Refl+  heq1 (Bound m) (Bound n) | m == n = Just Refl+  heq1 (Abs e1) (Abs e2) = cong <$> heq1 e1 e2+  heq1 (App o1 es1) (App o2 es2)+    | Just Refl ← heq1 o1 o2+    , Just Refl ← heq1 es1 es2 = Just Refl+  heq1 _ _ = Nothing  shiftVar   ∷ Var@@ -99,7 +103,7 @@   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 $ rmap (shiftVar v n) es+  App p es → App p $ shiftVar v n <<$>> es  addVar   ∷ Var@@ -110,7 +114,7 @@   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 $ rmap (addVar v n) es+  App p es → App p $ addVar v n <<$>> es  instance Show1 o ⇒ Abt Var o (Tm o) where   into = \case@@ -125,3 +129,23 @@       v ← fresh       return $ v :\ addVar v 0 e     App p es → return $ p :$ es++-- | A prism to extract arguments from a proposed operator.+--+-- @+-- '_TmOp' ∷ 'HEq1' o ⇒ o ns → Prism' ('Tm0' o) ('Rec' ('Tm0' o) ns)+-- @+--+_TmOp+  ∷ ( Choice p+    , Applicative f+    , HEq1 o+    )+  ⇒ o ns+  → p (Rec (Tm o) ns) (f (Rec (Tm o) ns))+  → p (Tm0 o) (f (Tm0 o))+_TmOp o = dimap fro (either pure (fmap (App o))) . right'+  where+    fro = \case+      App o' es | Just Refl ← heq1 o o' → Right es+      e → Left e
src/Abt/Tutorial.hs view
@@ -5,7 +5,9 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UnicodeSyntax #-}+{-# LANGUAGE ViewPatterns #-}  module Abt.Tutorial where @@ -16,7 +18,9 @@ import Control.Applicative import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Except import Data.Vinyl+import Prelude hiding (pi)  -- | We'll start off with a monad in which to manipulate ABTs; we'll need some -- state for fresh variable generation.@@ -48,19 +52,43 @@ -- indexed by arities. -- data Lang ns where-  Lam ∷ Lang '[S Z]-  Ap ∷ Lang '[Z,Z]+  LAM ∷ Lang '[S Z]+  APP ∷ Lang '[Z, Z]+  PI ∷ Lang '[Z, S Z]+  UNIT ∷ Lang '[]+  AX ∷ Lang '[]  instance Show1 Lang where   show1 = \case-    Lam → "lam"-    Ap → "ap"+    LAM → "lam"+    APP → "ap"+    PI → "pi"+    UNIT → "unit"+    AX → "<>"  instance HEq1 Lang where-  Lam === Lam = True-  Ap === Ap = True-  _ === _ = False+  heq1 LAM LAM = Just Refl+  heq1 APP APP = Just Refl+  heq1 PI PI = Just Refl+  heq1 UNIT UNIT = Just Refl+  heq1 AX AX = Just Refl+  heq1 _ _ = Nothing +lam ∷ Tm Lang (S Z) → Tm0 Lang+lam e = LAM $$ e :& RNil++app ∷ Tm0 Lang → Tm0 Lang → Tm0 Lang+app m n = APP $$ m :& n :& RNil++ax ∷ Tm0 Lang+ax = AX $$ RNil++unit ∷ Tm0 Lang+unit = UNIT $$ RNil++pi ∷ Tm0 Lang → Tm Lang (S Z) → Tm0 Lang+pi α xβ = PI $$ α :& xβ :& RNil+ -- | A monad transformer for small step operational semantics. -- newtype StepT m α@@ -86,12 +114,11 @@   → StepT M (Tm0 Lang) step tm =   out tm >>= \case-    Ap :$ m :& n :& RNil →+    APP :$ m :& n :& RNil →       out m >>= \case-        Lam :$ xe :& RNil → xe // n+        LAM :$ xe :& RNil → xe // n         _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n-          where-            app a b = Ap $$ a :& b :& RNil+    PI :$ α :& xβ :& RNil → pi <$> step α <*> pure xβ     _ → stepsExhausted  -- | The reflexive-transitive closure of a small-step operational semantics.@@ -109,29 +136,87 @@ eval ∷ Tm0 Lang → Tm0 Lang eval = runM . star step +newtype JudgeT m α+  = JudgeT+  { runJudgeT ∷ ExceptT String m α+  } deriving (Monad, Functor, Applicative, Alternative)++instance MonadVar Var m ⇒ MonadVar Var (JudgeT m) where+  fresh = JudgeT . ExceptT $ Right <$> fresh+  named str = JudgeT . ExceptT $ Right <$> named str++type Ctx = [(Var, Tm0 Lang)]++raise ∷ Monad m ⇒ String → JudgeT m α+raise = JudgeT . ExceptT . return . Left++checkTy+  ∷ Ctx+  → Tm0 Lang+  → Tm0 Lang+  → JudgeT M ()+checkTy g tm ty = do+  let ntm = eval tm+      nty = eval ty+  (,) <$> out ntm <*> out nty >>= \case+    (LAM :$ xe :& RNil, PI :$ α :& yβ :& RNil) → do+      z ← fresh+      ez ← xe // var z+      βz ← yβ // var z+      checkTy ((z,α):g) ez βz+    (AX :$ RNil, UNIT :$ RNil) → return ()+    _ → do+      ty' ← inferTy g tm+      if ty' === nty+        then return ()+        else raise "Type error"++inferTy+  ∷ Ctx+  → Tm0 Lang+  → JudgeT M (Tm0 Lang)+inferTy g tm = do+  out (eval tm) >>= \case+    V v | Just (eval → ty) ← lookup v g → return ty+        | otherwise → raise "Ill-scoped variable"+    APP :$ m :& n :& RNil → do+      inferTy g m >>= out >>= \case+        PI :$ α :& xβ :& RNil → do+          checkTy g n α+          eval <$> xβ // n+        _ → raise "Expected pi type for lambda abstraction"+    _ → raise "Only infer neutral terms"+ -- | @λx.x@ -- identityTm ∷ M (Tm0 Lang) identityTm = do   x ← fresh-  return $ Lam $$ (x \\ var x) :& RNil+  return $ lam (x \\ var x)  -- | @(λx.x)(λx.x)@ -- appTm ∷ M (Tm0 Lang) appTm = do   tm ← identityTm-  return $ Ap $$ tm :& tm :& RNil+  return $ app tm tm  -- | A demonstration of evaluating (and pretty-printing). Output: -- -- @--- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@2.\@2]+-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@4.\@4] -- @ -- main ∷ IO () main = do-  let mm = runM $ appTm >>= toString-      mm' = runM $ appTm >>= toString . eval-  print $ mm ++ " ~>* " ++ mm'+  -- Try out the type checker+  either fail print . runM . runExceptT . runJudgeT $ do+    x ← fresh+    checkTy [] (lam (x \\ var x)) (pi unit (x \\ unit))++  print . runM $ do+    mm ← appTm+    mmStr ← toString mm+    mmStr' ← toString $ eval mm+    return $ mmStr ++ " ~>* " ++ mmStr'
src/Abt/Types/View.hs view
@@ -8,10 +8,15 @@ module Abt.Types.View ( View(..) , View0+, _ViewOp , mapView ) where +import Abt.Class.HEq1 import Abt.Types.Nat++import Control.Applicative+import Data.Profunctor import Data.Vinyl  -- | @v@ is the type of variables; @o@ is the type of operators parameterized@@ -39,4 +44,24 @@ mapView η = \case   V v → V v   v :\ e → v :\ η e-  o :$ es → o :$ rmap η es+  o :$ es → o :$ η <<$>> es++-- | A prism to extract arguments from a proposed operator.+--+-- @+-- '_ViewOp' ∷ 'HEq1' o ⇒ o ns → Prism' ('View0' v o φ) ('Rec' φ ns)+-- @+--+_ViewOp+  ∷ ( Choice p+    , Applicative f+    , HEq1 o+    )+  ⇒ o ns+  → p (Rec φ ns) (f (Rec φ ns))+  → p (View0 v o φ) (f (View0 v o φ))+_ViewOp o = dimap fro (either pure (fmap (o :$))) . right'+  where+    fro = \case+      o' :$ es | Just Refl ← heq1 o o' → Right es+      e → Left e