-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | A bare-bones calculus of constructions -- @package morte @version 1.1.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 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 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 -- | Syntax tree for expressions data Expr -- | 
--   Const c        ~  c
--
Const :: Const -> Expr -- | 
--   Var (V x 0)    ~  x
--   Var (V x n)    ~  x@n
--
Var :: Var -> Expr -- | 
--   Lam x     A b  ~  λ(x : A) → b
--
Lam :: Text -> Expr -> Expr -> Expr -- | 
--   Pi x      A B  ~  ∀(x : A) → B
--   Pi unused A B  ~        A  → B
--
Pi :: Text -> Expr -> Expr -> Expr -- | 
--   App f a        ~  f a
--
App :: Expr -> Expr -> Expr -- | 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)] -- | 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 -> Either TypeError Expr -- | 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 -> Either TypeError Expr -- | 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 -> Expr -- | Determine whether a Pi-bound variable should be displayed -- -- Notice that if any variable within the body of a Pi shares the -- same name and an equal or greater DeBruijn index we display the -- Pi-bound variable. To illustrate why we don't just check for -- equality, consider this type: -- -- 
--   forall (a : *) -> forall (a : *) -> a@1
--
-- -- The a@1 refers to the outer a (i.e. the left one), -- but if we hid the inner a (the right one), the type would -- make no sense: -- -- 
--   forall (a : *) -> * -> a@1
--
-- -- ... because the a@1 would misleadingly appear to be an -- unbound variable. used :: Text -> Expr -> Bool -- | shift n x adds n to the index of all free variables -- named x within an Expr shift :: Int -> Text -> Expr -> Expr -- | Pretty-print an expression -- -- The result is a syntactically valid Morte program prettyExpr :: Expr -> Text -- | Pretty-print a type error prettyTypeError :: TypeError -> Text -- | A structured type error that includes context data TypeError TypeError :: Context -> Expr -> TypeMessage -> TypeError context :: TypeError -> Context current :: TypeError -> Expr typeMessage :: TypeError -> TypeMessage -- | The specific type error data TypeMessage UnboundVariable :: TypeMessage InvalidInputType :: Expr -> TypeMessage InvalidOutputType :: Expr -> TypeMessage NotAFunction :: TypeMessage TypeMismatch :: Expr -> Expr -> TypeMessage Untyped :: Const -> TypeMessage -- | Render a pretty-printed Const as a Builder buildConst :: Const -> Builder -- | Render a pretty-printed Var as a Builder buildVar :: Var -> Builder -- | Render a pretty-printed Expr as a Builder buildExpr :: Expr -> Builder -- | Render a pretty-printed TypeMessage as a Builder buildTypeMessage :: TypeMessage -> Builder -- | Render a pretty-printed TypeError as a Builder buildTypeError :: TypeError -> Builder instance Typeable TypeError instance Eq Var instance Show Var instance Eq Const instance Show Const instance Bounded Const instance Enum Const instance Show Expr instance Show TypeMessage instance NFData TypeError instance Exception TypeError instance Show TypeError instance NFData TypeMessage instance NFData Expr instance IsString Expr instance Binary Expr instance Eq Expr instance NFData Const instance Binary Const 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 -- | Pretty-print a ParseError prettyParseError :: ParseError -> Text -- | 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 Exception ParseError instance Show ParseError instance Error ParseMessage -- | 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