-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A bare-bones calculus of constructions -- @package morte @version 1.2.1 -- | 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 Token (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 :: String -> 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 instance Show Position instance Show Token instance Functor AlexLastAcc -- | 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 :: String -> 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 -- | 
--   Import path    ~  #path
--
Import :: 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). type Context = [(Text, Expr X)] -- | 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 -> 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 -> TypeMessage -> TypeError context :: TypeError -> Context 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 Typeable TypeError instance Eq Var instance Show Var instance Eq Const instance Show Const instance Bounded Const instance Enum Const instance Eq Path instance Ord Path instance Show Path instance Functor Expr instance Foldable Expr instance Traversable Expr instance Show a => Show (Expr a) instance Show TypeMessage instance Buildable TypeError instance NFData TypeError instance Exception TypeError instance Show TypeError instance Buildable TypeMessage instance NFData TypeMessage instance Buildable a => Buildable (Expr a) instance NFData a => NFData (Expr a) instance IsString (Expr a) instance Binary a => Binary (Expr a) instance Eq a => Eq (Expr a) instance Monad Expr instance Applicative Expr instance Buildable X instance NFData X instance Show X instance Eq X instance Buildable Path instance Buildable Const instance NFData Const instance Binary Const instance Buildable Var instance NFData Var instance IsString Var instance Binary Var -- | 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 Parsing :: Token -> ParseMessage instance Typeable ParseError instance Show ParseMessage instance Buildable ParseError instance Exception ParseError instance Show ParseError instance Error ParseMessage -- | 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 prepend the file path -- with a hash tag. For example, suppose we had the following three local -- files: -- -- 
--   -- id
--   \(a : *) -> \(x : a) -> x
--
-- -- 
--   -- Bool
--   forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True
--
-- -- 
--   -- 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)
--
-- -- 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 -- a hashtag followed by a 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 load :: Expr Path -> IO (Expr X) -- | An import failed because of a cycle import 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: -- -- 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 Typeable Cycle instance Typeable ReferentiallyOpaque instance Typeable Imported instance Show e => Show (Imported e) instance Exception e => Exception (Imported e) instance Show ReferentiallyOpaque instance Exception ReferentiallyOpaque instance Show Cycle instance Exception Cycle -- | 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