Dictionary-passing style

.ghci.repl

@@ -32,12 +32,14 @@
 -- 8.10+
 :seti -Wno-missing-safe-haskell-mode
 :seti -Wno-prepositive-qualified-module
+-- 9.2+
+:seti -Wno-missing-kind-signatures
 
 -- We have this one on in the project but not in the REPL to reduce noise
 :seti -Wno-type-defaults
 :set -Wno-unused-packages
 
-:load Facet.CLI test/Test.hs
+:load Facet.CLI Facet.Elab.Sequent test/Test.hs
 
 import Facet.Parser
 import Facet.Print

.github/workflows/ci.yml

@@ -14,14 +14,13 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        ghc: ["8.10.4"]
-        cabal: ["3.2.0.0"]
+        ghc: ["8.10", "9.2"]
 
     steps:
     - uses: actions/checkout@v2
       if: github.event.action == 'opened' || github.event.action == 'synchronize' || github.event.ref == 'refs/heads/main'
 
-    - uses: actions/setup-haskell@v1.1.4
+    - uses: haskell/actions/setup@v1
       name: Setup Haskell
       with:
         ghc-version: ${{ matrix.ghc }}

.hlint.yaml

@@ -0,0 +1 @@
+- ignore: {name: Use camelCase}

TODO.md

@@ -60,6 +60,10 @@ _Caveat lector: there are no guarantees of correctness or completeness on the co
 
   - Ideally, emit DWARF data.
 
+- Type patterns, for use with type lambdas & probably quantifiers.
+
+- Dictionary patterns, to bind the operations of an effect interface in the scope of a handler.
+
 
 ### Surface
 
@@ -144,11 +148,15 @@ _Caveat lector: there are no guarantees of correctness or completeness on the co
 
 ### Elaborator
 
-- Emit warnings.
+- ✅ Emit warnings.
 
 - Continue after errors on a declaration-by-declaration basis.
 
-- Add entire composite patterns to contexts. One entry for the whole pattern at type A, with sub-entries for each sub-pattern at decomposed types.
+- ✅ Add entire composite patterns to contexts. One entry for the whole pattern at type A, with sub-entries for each sub-pattern at decomposed types.
+
+- `Level`/`Level` pairs could be represented as `Ratio`s.
+
+- Distinguish between the `Level` a variable was bound and the `Level` of the place it’s being inserted at the type level using `newtype`s.
 
 
 ### Pretty-printer

docs/handlers.md

@@ -0,0 +1,65 @@
+# Handlers
+
+Handlers have the general form:
+
+    handle : C̅ -> [E̅] A -> B
+
+Typically, `A` will be parametric, and `B` can be viewed as a function of `A` and the context type(s) `C̅`. We will call `A` the incremental return type—that is, the return type of the action—and `B` the eventual return type—the return type of the handler itself.
+
+
+Handlers are defined by providing a list of clauses for the constructors in `E̅` and a list of clauses for non-effect values at type `A`. The former define a dictionary for `E̅`, and the latter define a continuation with which to run the body. Ignoring for the moment any context arguments of type `C̅`, that gives us:
+
+    { [o̅ x̅ ; k̅] -> b̅
+    , a̅         -> b̅ }
+
+where
+
+    o̅ : X̅ -> X′
+    x̅ : X̅
+    k̅ : X′ -> [E̅] A
+    a̅ : A
+    b̅ : B
+
+Note that since `k̅` returns in `[E̅] A`, clauses which use the continuation must call the handler recursively on the result. The sole exception is that if `B` is `[E̅] A`, they can technically call the continuation without calling the handler recursively. Note however that this would be _extremely_ strange as it would amount to handling only the first operation within an effect and allowing the remainder to be handled by the calling context.
+
+For example, we have the following types for the operations of `State S`, `Reader R`, and `Empty`:
+
+```facet
+# State S
+get : [State S] S
+put : S -> [State S] Unit
+
+# Reader R
+ask : [Reader R] R
+local : {X : Type} -> (R -> R) -> [Reader R] X -> [Reader R] X
+
+# Empty
+empty : {X : Type} -> [Empty] X
+```
+
+Note that all of these return computation types.
+
+Translating them into CPS yields:
+
+```facet
+# State S
+get : (S -> [State S] A) -> B
+put : S -> (Unit -> [State S] A) -> B
+
+# Reader R
+ask : (R -> [Reader R] A) -> B
+local : {X : Type} -> (R -> R) -> [Reader R] X -> (X -> [Reader R] A) -> B
+
+# Empty
+empty : {X : Type} -> [Empty] X
+```
+
+
+Scoped operations like `local` and `catch` themselves contain `E̅`-actions.
+
+
+Handlers must be able to:
+
+1. return a value of type `B` directly, without calling the continuation `k`. This implies that the type of handlers must not be universally quantified with respect to its eventual return type.
+
+2. return a value of type `X′` by calling the continuation `k`, thus producing a result of type `A` with effects in `E̅`, which it must therefore handle by calling itself recursively.

facet.cabal

@@ -70,88 +70,109 @@ common common
 library
   import: common
   exposed-modules:
-    Facet.Carrier.Error.Lens
+    Facet.Carrier.CallStack.Stack
+    Facet.Carrier.Error.Optic
     Facet.Carrier.Output.IO
     Facet.Carrier.Parser.Church
     Facet.Carrier.Profile.Flat
     Facet.Carrier.Profile.Identity
     Facet.Carrier.Profile.Tree
     Facet.Carrier.Readline.Haskeline
-    Facet.Carrier.State.Lens
+    Facet.Carrier.State.Optic
     Facet.Carrier.Throw.Inject
     Facet.Carrier.Time.System
     Facet.Carrier.Write.General
     Facet.Carrier.Write.Inject
     Facet.CLI
     Facet.Context
-    Facet.Core.Module
-    Facet.Core.Pattern
-    Facet.Core.Term
-    Facet.Core.Type
     Facet.Diff
     Facet.Driver
+    Facet.Effect.CallStack
     Facet.Effect.Parser
     Facet.Effect.Profile
     Facet.Effect.Readline
     Facet.Effect.Time
     Facet.Effect.Time.System
     Facet.Effect.Write
     Facet.Elab
+    Facet.Elab.Sequent
     Facet.Elab.Term
     Facet.Elab.Type
     Facet.Env
     Facet.Eval
     Facet.Flag
     Facet.Format
+    Facet.Functor.Check
+    Facet.Functor.Compose
+    Facet.Functor.Synth
     Facet.Graph
+    Facet.Interface
+    Facet.Kind
     Facet.Lens
     Facet.Lexer
+    Facet.Module
     Facet.Name
-    Facet.Norm
     Facet.Notice
     Facet.Notice.Elab
     Facet.Notice.Parser
     Facet.Parser
     Facet.Parser.Table
+    Facet.Pattern
+    Facet.Pattern.Column
     Facet.Pretty
     Facet.Print
+    Facet.Print.Options
+    Facet.Quote
     Facet.REPL
     Facet.REPL.Parser
     Facet.Run
+    Facet.Scope
     Facet.Semialign
-    Facet.Semiring
+    Facet.Sequent.Expr
+    Facet.Sequent.Pattern
+    Facet.Sequent.Type
     Facet.Snoc
     Facet.Snoc.NonEmpty
     Facet.Source
+    Facet.Source.Reference
     Facet.Span
     Facet.Style
     Facet.Subst
-    Facet.Surface
+    Facet.Surface.Module
+    Facet.Surface.Term.Expr
+    Facet.Surface.Type.Class
+    Facet.Surface.Type.Expr
     Facet.Syntax
+    Facet.Term.Class
+    Facet.Term.Expr
+    Facet.Term.Norm
     Facet.Timing
+    Facet.Type.Class
+    Facet.Type.Expr
+    Facet.Type.Norm
+    Facet.TypeContext
     Facet.Unify
-    Facet.Usage
     Facet.Vars
   other-modules:
     Paths_facet
   autogen-modules:
     Paths_facet
   build-depends:
     , ansi-terminal
-    , base >= 4.14 && < 4.21
+    , base >= 4.14 && < 5
     , charset
     , colour
     , containers
     , directory
     , exceptions ^>= 0.10
     , filepath
+    , fresnel
     , fused-effects
-    , fused-effects-lens
     , haskeline ^>= 0.8.1
-    , lens
     , optparse-applicative
     , parsers
     , prettyprinter
+    , profunctors
     , semialign
     , silkscreen
     , terminal-size
@@ -178,8 +199,9 @@ test-suite test
     , facet
     , hedgehog ^>= 1.5
     , parsers
-  ghc-options:
-    -Wno-missing-signatures
+  if (impl(ghc >= 9.2))
+    ghc-options:
+      -Wno-missing-signatures
 
 
 executable facetc

lib/Effect/Empty.facet

@@ -2,10 +2,16 @@ module Effect.Empty : Module
 
 import Data.Bool
 import Data.Function
+import Data.Option
 import Data.Unit
 
 interface Empty : Interface
 { empty : { A : Type } -> A }
 
 guard : (c : Bool) -> [Empty] Unit
 { if c id { (unit) -> empty } }
+
+
+toOption : {A : Type} -> [Empty] A -> Option A
+{ [empty ; _] -> none
+, a           -> some a }

script/ghci-flags

@@ -66,8 +66,9 @@ function flags {
   echo "-Wno-name-shadowing"
   echo "-Wno-safe"
   echo "-Wno-unsafe"
-  [[ "$ghc_version" = 8.8.* ]] || [[ "$ghc_version" = 8.10.* ]] && echo "-Wno-missing-deriving-strategies" || true
-  [[ "$ghc_version" = 8.10.* ]] && echo "-Wno-missing-safe-haskell-mode" && echo "-Wno-prepositive-qualified-module" && echo "-Wno-unused-packages"
+  [[ "$ghc_version" = 8.8.* ]] || [[ "$ghc_version" = 8.10.* ]] || [[ "$ghc_version" = 9.2.* ]] && echo "-Wno-missing-deriving-strategies" || true
+  [[ "$ghc_version" = 8.10.* ]] || [[ "$ghc_version" = 9.2.* ]] && echo "-Wno-missing-safe-haskell-mode" && echo "-Wno-prepositive-qualified-module" && echo "-Wno-unused-packages"
+  [[ "$ghc_version" = 9.2.* ]] && echo "-Wno-missing-kind-signatures"
 
   echo "-XDeriveTraversable"
   echo "-XDerivingStrategies"

src/Facet/Carrier/CallStack/Stack.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Facet.Carrier.CallStack.Stack
+( -- * CallStack carrier
+  runCallStack
+, CallStackC(..)
+  -- * CallStack effect
+, module Facet.Effect.CallStack
+) where
+
+import Control.Algebra
+import Control.Carrier.Reader
+import Facet.Effect.CallStack
+
+runCallStack :: CallStackC m a -> m a
+runCallStack = runReader [] . runCallStackC
+
+newtype CallStackC m a = CallStackC { runCallStackC :: ReaderC Stack m a }
+  deriving (Applicative, Functor, Monad)
+
+instance Algebra sig m => Algebra (CallStack :+: sig) (CallStackC m) where
+  alg hdl sig ctx = CallStackC $ case sig of
+    L (Push l s m) -> local ((l, s):) (runCallStackC (hdl (m <$ ctx)))
+    L CallStack    -> asks (<$ ctx)
+    R other        -> alg (runCallStackC . hdl) (R other) ctx

src/Facet/Carrier/Error/Lens.hs → src/Facet/Carrier/Error/Optic.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE UndecidableInstances #-}
-module Facet.Carrier.Error.Lens
+module Facet.Carrier.Error.Optic
 ( -- * Error carrier
   runError
 , ErrorC(..)
@@ -11,17 +11,21 @@ module Facet.Carrier.Error.Lens
 import Control.Algebra
 import Control.Carrier.Reader
 import Control.Effect.Error
-import Control.Lens (APrism', withPrism)
 import Control.Monad.IO.Class
+import Fresnel.Prism (Prism', matching)
+import Fresnel.Review (review)
 
-runError :: APrism' e f -> ErrorC e f m a -> m a
-runError prism (ErrorC m) = runReader prism m
+runError :: Prism' e f -> ErrorC e f m a -> m a
+runError prism (ErrorC m) = runReader (APrism' prism) m
 
 newtype ErrorC e f m a = ErrorC (ReaderC (APrism' e f) m a)
   deriving (Applicative, Functor, Monad, MonadFail, MonadIO)
 
 instance Has (Error e) sig m => Algebra (Error f :+: sig) (ErrorC e f m) where
-  alg hdl sig ctx = ErrorC $ ReaderC $ \ prism -> case sig of
-    L (L (Throw e))   -> throwError (withPrism prism (\ review _ -> review e))
-    L (R (Catch m h)) -> runError prism (hdl (m <$ ctx)) `catchError` \ e -> withPrism prism (\ _ preview -> either throwError (runError prism . hdl . (<$ ctx) . h) (preview e))
+  alg hdl sig ctx = ErrorC $ ReaderC $ \ (APrism' prism) -> case sig of
+    L (L (Throw e))   -> throwError (review prism e)
+    L (R (Catch m h)) -> runError prism (hdl (m <$ ctx)) `catchError` \ e -> either throwError (runError prism . hdl . (<$ ctx) . h) (matching prism e)
     R other           -> alg (runError prism . hdl) other ctx
+
+
+newtype APrism' s a = APrism' (Prism' s a)

src/Facet/Carrier/Parser/Church.hs

@@ -26,20 +26,22 @@ import Control.Algebra
 import Control.Effect.Cut
 import Control.Effect.NonDet
 import Control.Effect.Throw
-import Control.Lens (Lens', lens, (%~), (&), (.~))
 import Control.Monad (ap)
 import Control.Monad.Fail as Fail
 import Control.Monad.Fix
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Class
 import Data.Coerce (coerce)
+import Data.Function ((&))
 import Data.Functor.Compose
 import Data.Functor.Identity
 import Data.List.NonEmpty (NonEmpty(..))
 import Data.Set (Set, singleton)
 import Facet.Effect.Parser
 import Facet.Source as Source
 import Facet.Span as Span
+import Fresnel.Lens (Lens', lens)
+import Fresnel.Setter ((%~), (.~))
 import Text.Parser.Char (CharParsing(..))
 import Text.Parser.Combinators
 import Text.Parser.Token (TokenParsing)
@@ -55,7 +57,7 @@ runParserWithFile path p = do
 {-# INLINE runParserWithFile #-}
 
 runParserWithSource :: Has (Throw (Source, Err)) sig m => Source -> ParserC m a -> m a
-runParserWithSource src@(Source _ _ _ (Line line _ _:|_)) = runParser (const pure) failure failure input
+runParserWithSource src@(Source _ _ (Line line _ _:|_)) = runParser (const pure) failure failure input
   where
   input = Input (Pos line 0) (contents src)
   failure = throwError . (,) src