-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A bare-bones calculus of constructions -- -- Morte is a typed, purely functional, and strongly normalizing -- intermediate language designed for whole-program super-optimization. -- Use this library to type-check, optimize, parse, pretty-print, -- serialize and deserialize expressions in this intermediate language. -- -- This library also installs an executable that you can use to -- type-check and optimize a morte program. -- -- Morte.Core contains the core calculus of constructions for this -- language -- -- Morte.Lexer contains the alex-generated lexer for -- Morte -- -- Morte.Parser contains the parser for Morte -- -- Read Morte.Tutorial to learn how to use this library @package morte @version 1.6.2 -- | Lexing logic for the Morte language module Morte.Lexer -- | Convert a text representation of an expression into a stream of tokens -- -- lexExpr keeps track of position and returns the remainder of -- the input if lexing fails. lexExpr :: Text -> Producer LocatedToken (State Position) (Maybe Text) -- | Token type, used to communicate between the lexer and parser data Token OpenParen :: Token CloseParen :: Token Colon :: Token At :: Token Star :: Token Box :: Token Arrow :: Token Lambda :: Token Pi :: Token Label :: Text -> Token Number :: Int -> Token File :: FilePath -> Token URL :: Text -> Token EOF :: Token -- | The cursor's location while lexing the text data Position P :: {-# UNPACK #-} !Int -> {-# UNPACK #-} !Int -> Position [lineNo] :: Position -> {-# UNPACK #-} !Int [columnNo] :: Position -> {-# UNPACK #-} !Int -- | A Token augmented with Position information data LocatedToken LocatedToken :: !Token -> {-# UNPACK #-} !Position -> LocatedToken [token] :: LocatedToken -> !Token [position] :: LocatedToken -> {-# UNPACK #-} !Position instance GHC.Show.Show Morte.Lexer.LocatedToken instance GHC.Show.Show Morte.Lexer.Token instance GHC.Classes.Eq Morte.Lexer.Token instance GHC.Show.Show Morte.Lexer.Position instance GHC.Base.Functor Morte.Lexer.AlexLastAcc -- | All Context-related operations module Morte.Context -- | Bound variable names and their types -- -- Variable names may appear more than once in the Context. The -- Var x@n refers to the nth occurrence of -- x in the Context (using 0-based numbering). data Context a -- | An empty context with no key-value pairs -- -- 
--   toList empty = []
--
empty :: Context a -- | Add a key-value pair to the Context insert :: Text -> a -> Context a -> Context a -- | Lookup a key by name and index -- -- 
--   lookup k 0 (insert k v0              ctx ) = Just v0
--   lookup k 1 (insert k v0 (insert k v1 ctx)) = Just v1
--
lookup :: Text -> Int -> Context a -> Maybe a -- | Return all key-value associations as a list toList :: Context a -> [(Text, a)] instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Morte.Context.Context a) instance GHC.Base.Functor Morte.Context.Context -- | This module contains the core calculus for the Morte language. This -- language is a minimalist implementation of the calculus of -- constructions, which is in turn a specific kind of pure type system. -- If you are new to pure type systems you may wish to read "Henk: a -- typed intermediate language". -- -- -- http://research.microsoft.com/en-us/um/people/simonpj/papers/henk.ps.gz -- -- Morte is a strongly normalizing language, meaning that: -- -- -- -- Strong normalization comes at a price: Morte forbids recursion. -- Instead, you must translate all recursion to F-algebras and translate -- all corecursion to F-coalgebras. If you are new to F-(co)algebras then -- you may wish to read Morte.Tutorial or read "Recursive types -- for free!": -- -- -- http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt -- -- Morte is designed to be a super-optimizing intermediate language with -- a simple optimization scheme. You optimize a Morte expression by just -- normalizing the expression. If you normalize a long-lived program -- encoded as an F-coalgebra you typically get a state machine, and if -- you normalize a long-lived program encoded as an F-algebra you -- typically get an unrolled loop. -- -- Strong normalization guarantees that all abstractions encodable in -- Morte are "free", meaning that they may increase your program's -- compile times but they will never increase your program's run time -- because they will normalize to the same code. module Morte.Core -- | Label for a bound variable -- -- The Text field is the variable's name (i.e. "x"). -- -- The Int field disambiguates variables with the same name if -- there are multiple bound variables of the same name in scope. Zero -- refers to the nearest bound variable and the index increases by one -- for each bound variable of the same name going outward. The following -- diagram may help: -- -- 
--                             +-refers to-+
--                             |           |
--                             v           |
--   \(x : *) -> \(y : *) -> \(x : *) -> x@0
--   
--     +-------------refers to-------------+
--     |                                   |
--     v                                   |
--   \(x : *) -> \(y : *) -> \(x : *) -> x@1
--
-- -- This Int behaves like a De Bruijn index in the special case -- where all variables have the same name. -- -- You can optionally omit the index if it is 0: -- -- 
--                             +refers to+
--                             |         |
--                             v         |
--   \(x : *) -> \(y : *) -> \(x : *) -> x
--
-- -- Zero indices are omitted when pretty-printing Vars and non-zero -- indices appear as a numeric suffix. data Var V :: Text -> Int -> Var -- | Constants for the calculus of constructions -- -- The only axiom is: -- -- 
--   ⊦ * : □
--
-- -- ... and all four rule pairs are valid: -- -- 
--   ⊦ * ↝ * : *
--   ⊦ □ ↝ * : *
--   ⊦ * ↝ □ : □
--   ⊦ □ ↝ □ : □
--
data Const Star :: Const Box :: Const -- | Path to an external resource data Path File :: FilePath -> Path URL :: Text -> Path -- | Like Void, except with an NFData instance in order to -- avoid orphan instances newtype X X :: (forall a. a) -> X [absurd] :: X -> forall a. a -- | Syntax tree for expressions data Expr a -- | 
--   Const c        ~  c
--
Const :: Const -> Expr a -- | 
--   Var (V x 0)    ~  x
--   Var (V x n)    ~  x@n
--
Var :: Var -> Expr a -- | 
--   Lam x     A b  ~  λ(x : A) → b
--
Lam :: Text -> (Expr a) -> (Expr a) -> Expr a -- | 
--   Pi x      A B  ~  ∀(x : A) → B
--   Pi unused A B  ~        A  → B
--
Pi :: Text -> (Expr a) -> (Expr a) -> Expr a -- | 
--   App f a        ~  f a
--
App :: (Expr a) -> (Expr a) -> Expr a -- | 
--   Embed path     ~  #path
--
Embed :: a -> Expr a -- | Bound variable names and their types -- -- Variable names may appear more than once in the Context. The -- Var x@n refers to the nth occurrence of -- x in the Context (using 0-based numbering). data Context a -- | Type-check an expression and return the expression's type if -- type-checking suceeds or an error if type-checking fails -- -- typeWith does not necessarily normalize the type since full -- normalization is not necessary for just type-checking. If you actually -- care about the returned type then you may want to normalize it -- afterwards. typeWith :: Context (Expr X) -> Expr X -> Either TypeError (Expr X) -- | typeOf is the same as typeWith with an empty context, -- meaning that the expression must be closed (i.e. no free variables), -- otherwise type-checking will fail. typeOf :: Expr X -> Either TypeError (Expr X) -- | Reduce an expression to its normal form, performing both beta -- reduction and eta reduction -- -- normalize does not type-check the expression. You may want to -- type-check expressions before normalizing them since normalization can -- convert an ill-typed expression into a well-typed expression. normalize :: Expr a -> Expr a -- | shift n x adds n to the index of all free variables -- named x within an Expr shift :: Int -> Text -> Expr a -> Expr a -- | Substitute all occurrences of a variable with an expression -- -- 
--   subst x n C B  ~  B[x@n := C]
--
subst :: Text -> Int -> Expr a -> Expr a -> Expr a -- | Pretty-print a value pretty :: Buildable a => a -> Text -- | A structured type error that includes context data TypeError TypeError :: Context (Expr X) -> Expr X -> TypeMessage -> TypeError [context] :: TypeError -> Context (Expr X) [current] :: TypeError -> Expr X [typeMessage] :: TypeError -> TypeMessage -- | The specific type error data TypeMessage UnboundVariable :: TypeMessage InvalidInputType :: (Expr X) -> TypeMessage InvalidOutputType :: (Expr X) -> TypeMessage NotAFunction :: TypeMessage TypeMismatch :: (Expr X) -> (Expr X) -> TypeMessage Untyped :: Const -> TypeMessage instance GHC.Show.Show Morte.Core.TypeMessage instance GHC.Show.Show a => GHC.Show.Show (Morte.Core.Expr a) instance Data.Traversable.Traversable Morte.Core.Expr instance Data.Foldable.Foldable Morte.Core.Expr instance GHC.Base.Functor Morte.Core.Expr instance GHC.Show.Show Morte.Core.Path instance GHC.Classes.Ord Morte.Core.Path instance GHC.Classes.Eq Morte.Core.Path instance GHC.Enum.Enum Morte.Core.Const instance GHC.Enum.Bounded Morte.Core.Const instance GHC.Show.Show Morte.Core.Const instance GHC.Classes.Eq Morte.Core.Const instance GHC.Show.Show Morte.Core.Var instance GHC.Classes.Eq Morte.Core.Var instance Data.Binary.Class.Binary Morte.Core.Var instance Data.String.IsString Morte.Core.Var instance Control.DeepSeq.NFData Morte.Core.Var instance Data.Text.Buildable.Buildable Morte.Core.Var instance Data.Binary.Class.Binary Morte.Core.Const instance Control.DeepSeq.NFData Morte.Core.Const instance Data.Text.Buildable.Buildable Morte.Core.Const instance Data.Text.Buildable.Buildable Morte.Core.Path instance GHC.Classes.Eq Morte.Core.X instance GHC.Show.Show Morte.Core.X instance Control.DeepSeq.NFData Morte.Core.X instance Data.Text.Buildable.Buildable Morte.Core.X instance Data.Binary.Class.Binary Morte.Core.X instance GHC.Base.Applicative Morte.Core.Expr instance GHC.Base.Monad Morte.Core.Expr instance GHC.Classes.Eq a => GHC.Classes.Eq (Morte.Core.Expr a) instance Data.Binary.Class.Binary a => Data.Binary.Class.Binary (Morte.Core.Expr a) instance Data.String.IsString (Morte.Core.Expr a) instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Morte.Core.Expr a) instance Data.Text.Buildable.Buildable a => Data.Text.Buildable.Buildable (Morte.Core.Expr a) instance Control.DeepSeq.NFData Morte.Core.TypeMessage instance Data.Text.Buildable.Buildable Morte.Core.TypeMessage instance GHC.Show.Show Morte.Core.TypeError instance GHC.Exception.Exception Morte.Core.TypeError instance Control.DeepSeq.NFData Morte.Core.TypeError instance Data.Text.Buildable.Buildable Morte.Core.TypeError -- | Parsing logic for the Morte language module Morte.Parser -- | Parse an Expr from Text or return a ParseError if -- parsing fails exprFromText :: Text -> Either ParseError (Expr Path) -- | Structured type for parsing errors data ParseError ParseError :: Position -> ParseMessage -> ParseError [position] :: ParseError -> Position [parseMessage] :: ParseError -> ParseMessage -- | The specific parsing error data ParseMessage -- | Lexing failed, returning the remainder of the text Lexing :: Text -> ParseMessage -- | Parsing failed, returning the invalid token and the expected tokens Parsing :: Token -> [Token] -> ParseMessage instance GHC.Show.Show Morte.Parser.ParseMessage instance GHC.Show.Show Morte.Parser.ParseError instance GHC.Exception.Exception Morte.Parser.ParseError instance Data.Text.Buildable.Buildable Morte.Parser.ParseError -- | Morte lets you import external expressions located either in local -- files or hosted on network endpoints. -- -- To import a local file as an expression, just insert the path to the -- file, prepending a ./ if the path is relative to the current -- directory. For example, suppose we had the following three local -- files: -- -- 
--   -- id
--   \(a : *) -> \(x : a) -> x
--
-- -- 
--   -- Bool
--   forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool
--
-- -- 
--   -- True
--   \(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True
--
-- -- You could then reference them within a Morte expression using this -- syntax: -- -- 
--   ./id ./Bool ./True
--
-- -- ... which would embed their expressions directly within the syntax -- tree: -- -- 
--   -- ... expands out to:
--   (\(a : *) -> \(x : a) -> x)
--       (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True)
--       (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True)
--
-- -- ... and which normalizes to: -- -- 
--   λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
--
-- -- Imported expressions may contain imports of their own, too, which will -- continue to be resolved. However, Morte will prevent cyclic imports. -- For example, if you had these two files: -- -- 
--   -- foo
--   ./bar
--
-- -- 
--   -- bar
--   ./foo
--
-- -- ... Morte would throw the following exception if you tried to import -- foo: -- -- 
--   morte: 
--   ⤷ ./foo
--   ⤷ ./bar
--   Cyclic import: ./foo
--
-- -- You can also import expressions hosted on network endpoints. Just use -- the URL -- -- 
--   http://host[:port]/path
--
-- -- The compiler expects the downloaded expressions to be in the same -- format as local files, specifically UTF8-encoded source code text. -- -- For example, if our id expression were hosted at -- http://example.com/id, then we would embed the -- expression within our code using: -- -- 
--   http://example.com/id
--
-- -- You can also reuse directory names as expressions. If you provide a -- path to a local or remote directory then the compiler will look for a -- file named @ within that directory and use that file to -- represent the directory. module Morte.Import -- | Resolve all imports within an expression -- -- By default the starting path is the current directory, but you can -- override the starting path with a file if you read in the expression -- from that file load :: Maybe Path -> Expr Path -> IO (Expr X) -- | An import failed because of a cycle in the import graph newtype Cycle Cycle :: Path -> Cycle -- | The offending cyclic import [cyclicImport] :: Cycle -> Path -- | Morte tries to ensure that all expressions hosted on network endpoints -- are weakly referentially transparent, meaning roughly that any two -- clients will compile the exact same result given the same URL. -- -- To be precise, a strong interpretaton of referential transparency -- means that if you compiled a URL you could replace the expression -- hosted at that URL with the compiled result. Let's term this "static -- linking". Morte (very intentionally) does not satisfy this stronger -- interpretation of referential transparency since "statically linking" -- an expression (i.e. permanently resolving all imports) means that the -- expression will no longer update if its dependencies change. -- -- In general, either interpretation of referential transparency is not -- enforceable in a networked context since one can easily violate -- referential transparency with a custom DNS, but Morte can still try to -- guard against common unintentional violations. To do this, Morte -- enforces that a non-local import may not reference a local import. -- -- Local imports are defined as: -- -- -- -- All other imports are defined to be non-local newtype ReferentiallyOpaque ReferentiallyOpaque :: Path -> ReferentiallyOpaque -- | The offending opaque import [opaqueImport] :: ReferentiallyOpaque -> Path -- | Extend another exception with the current import stack data Imported e Imported :: [Path] -> e -> Imported e -- | Imports resolved so far, in reverse order [importStack] :: Imported e -> [Path] -- | The nested exception [nested] :: Imported e -> e instance GHC.Exception.Exception Morte.Import.Cycle instance GHC.Show.Show Morte.Import.Cycle instance GHC.Exception.Exception Morte.Import.ReferentiallyOpaque instance GHC.Show.Show Morte.Import.ReferentiallyOpaque instance GHC.Exception.Exception e => GHC.Exception.Exception (Morte.Import.Imported e) instance GHC.Show.Show e => GHC.Show.Show (Morte.Import.Imported e) -- | Morte is a minimalist implementation of the calculus of constructions -- that comes with a parser, type-checker, optimizer, and pretty-printer. -- -- You can think of Morte as a very low-level intermediate language for -- functional languages. This virtual machine was designed with the -- following design principles, in descending order of importance: -- -- -- -- This library does not provide any front-end or back-end language for -- Morte. These will be provided as separate libraries in the future. -- -- The "Introduction" section walks through basic usage of the compiler -- and library. -- -- The "Desugaring" section explains how to desugar complex abstractions -- to Morte's core calculus. -- -- The "Optimization" section explains how Morte optimizes programs, -- providing several long-form example programs and their optimized -- output. module Morte.Tutorial