annah (empty) → 1.0.0

raw patch · 8 files changed

+3020/−0 lines, 8 filesdep +Earleydep +annahdep +arraysetup-changed

Dependencies added: Earley, annah, array, base, lens-family-core, morte, optparse-applicative, pipes, system-fileio, system-filepath, text, text-format, transformers

Files

• LICENSE +24/−0
• Setup.hs +2/−0
• annah.cabal +72/−0
• exec/Main.hs +154/−0
• src/Annah/Core.hs +594/−0
• src/Annah/Lexer.x +215/−0
• src/Annah/Parser.hs +260/−0
• src/Annah/Tutorial.hs +1699/−0

@@ -0,0 +1,24 @@+Copyright (c) 2014 Gabriel Gonzalez+All rights reserved.++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:+    * Redistributions of source code must retain the above copyright notice,+      this list of conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright notice,+      this list of conditions and the following disclaimer in the documentation+      and/or other materials provided with the distribution.+    * Neither the name of Gabriel Gonzalez nor the names of other contributors+      may be used to endorse or promote products derived from this software+      without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,72 @@+Name: annah+Version: 1.0.0+Cabal-Version: >=1.8.0.2+Build-Type: Simple+Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2+License: BSD3+License-File: LICENSE+Copyright: 2015 Gabriel Gonzalez+Author: Gabriel Gonzalez+Maintainer: Gabriel439@gmail.com+Bug-Reports: https://github.com/Gabriel439/Haskell-Annah-Library/issues+Synopsis: Medium-level language that desugars to Morte+Description: Annah is a very simple statically typed and purely functional+    lambda calculus with built-in support for:+    .+    * imports via embedding remote expressions+    .+    * mutually recursive data types+    .+    * let expressions+    .+    * natural numbers+    .+    * lists+    .+    * free monads+    .+    * free categories+    .+    Annah is built on top of Morte (a minimalist calculus of constructions),+    meaning that all language features that Annah provides are desugared to+    a pure non-recursive lambda calculus.+    .+    Read the "Annah.Tutorial" module to learn more about how to program using+    Annah.+Category: Compiler+Source-Repository head+    Type: git+    Location: https://github.com/Gabriel439/Haskell-Annah-Library++Library+    Hs-Source-Dirs: src+    Build-Depends:+        base             >= 4        && < 5   ,+        array            >= 0.4.0.0  && < 0.6 ,+        Earley           >= 0.10.1.0 && < 0.12,+        lens-family-core >= 1.0.0    && < 1.3 ,+        morte            >= 1.6.0    && < 1.7 ,+        pipes            >= 4.0.0    && < 4.2 ,+        system-filepath  >= 0.3.1    && < 0.5 ,+        text             >= 0.11.1.0 && < 1.3 ,+        text-format                     < 0.4 ,+        transformers     >= 0.2.0.0  && < 0.5+    Exposed-Modules:+        Annah.Core,+        Annah.Lexer,+        Annah.Parser,+        Annah.Tutorial+    Build-Tools: alex+    GHC-Options: -O2++Executable annah+    Hs-Source-Dirs: exec+    Main-Is: Main.hs+    Build-Depends:+        base                 >= 4        && < 5   ,+        annah                                     ,+        morte                >= 1.6.0    && < 1.7 ,+        optparse-applicative                < 0.13,+        system-filepath      >= 0.3.1    && < 0.5 ,+        system-fileio        >= 0.2.1    && < 0.4 ,+        text                 >= 0.11.1.0 && < 1.3

@@ -0,0 +1,154 @@+{-# LANGUAGE OverloadedStrings #-}++module Main where++import Annah.Core (Data(..), Expr(..), Type(..))+import Control.Applicative ((<|>))+import Control.Exception (Exception, throwIO)+import Control.Monad (forM_)+import Data.Monoid (mempty)+import Data.Text.Lazy (fromStrict)+import Filesystem.Path (FilePath, (</>))+import Morte.Core (Path(..), Var(..))+import Options.Applicative+import Prelude hiding (FilePath)+import System.IO (stderr)++import qualified Annah.Core                as Annah+import qualified Annah.Parser              as Annah+import qualified Data.Text.Lazy            as Text+import qualified Data.Text.Lazy.IO         as Text+import qualified Filesystem+import qualified Filesystem.Path.CurrentOS as Filesystem+import qualified Morte.Core                as Morte+import qualified Morte.Import              as Morte++throws :: Exception e => Either e a -> IO a+throws (Left  e) = throwIO e+throws (Right r) = return r++data Mode = Default | Compile FilePath | Desugar | Types++parser :: Parser Mode+parser+    =   subparser+        (   command "compile"+            (info (helper <*> (Compile <$> parseFilePath))+                (   fullDesc+                <>  header "annah compile - Compile Annah code"+                <>  progDesc "Compile an Annah program located at the given \+                             \file path.  Prefer this subcommand over reading \+                             \from standard input when you want remote \+                             \references to be resolved relative to that \+                             \file's path"+                )+            )+        <>  metavar "compile"+        )+    <|> subparser+        (   command "desugar"+            (info (helper <*> pure Desugar)+                (   fullDesc+                <>  header "annah desugar - Desugar Annah code"+                <>  progDesc "Desugar an Annah program to the equivalent Morte \+                             \program, reading the Annah program from standard \+                             \input and writing the Morte program to standard \+                             \output."+                )+            )+        <>  metavar "desugar"+        )+    <|> subparser+        (   command "types"+            (   info (helper <*> pure Types)+                (   fullDesc+                <>  header "annah types - Compile an Annah datatype definition"+                <>  progDesc "Translate an Annah datatype definition to the \+                             \equivalent set of files, reading the datatype \+                             \definition from standard input.  This creates \+                             \one output directory for each type with one file \+                             \underneath each directory per data constructor \+                             \associated with that type."+                )+            )+        <>  metavar "types"+        )+    <|> pure Default+  where+    parseFilePath =+        fmap Filesystem.decodeString+            (strArgument (metavar "FILEPATH" <> help "Path to file to compile"))++main :: IO ()+main = do+    mode <- execParser $ info (helper <*> parser)+        (   fullDesc+        <>  header "annah - A strongly typed, purely functional language"+        <>  progDesc "Annah is a medium-level language that is a superset of \+                     \Morte.  Use this compiler to desugar Annah code to Morte \+                     \code."+        )+    case mode of+        Default -> do+            txt <- Text.getContents+            ae  <- throws (Annah.exprFromText txt)+            let me = Annah.desugar ae+            -- Only statically link the Morte expression for type-checking+            me' <- Morte.load Nothing me+            mt  <- throws (Morte.typeOf me')+            -- Return the dynamically linked Morte expression+            Text.putStrLn (Morte.pretty (Morte.normalize me))+        Compile file -> do+            txt <- Text.readFile (Filesystem.encodeString file)+            ae  <- throws (Annah.exprFromText txt)+            let me = Annah.desugar ae+            -- Only statically link the Morte expression for type-checking+            me' <- Morte.load (Just (File file)) me+            mt  <- throws (Morte.typeOf me')+            -- Return the dynamically linked Morte expression+            Text.putStrLn (Morte.pretty (Morte.normalize me))+        Desugar -> do+            txt <- Text.getContents+            ae  <- throws (Annah.exprFromText txt)+            Text.putStrLn (Morte.pretty (Annah.desugar ae))+        Types -> do+            -- TODO: Handle duplicate type and data constructor names+            txt <- Text.getContents+            ts  <- throws (Annah.typesFromText txt)+            let write file txt =+                    Filesystem.writeTextFile file (Text.toStrict txt <> "\n")+            let named = Filesystem.fromText . Text.toStrict+            forM_ ts (\t -> do+                let typeDir = named (typeName t)+                let typeAnnahFile = named (typeName t <> ".annah")+                let typeMorteFile = typeDir </> "@"+                let foldAnnahFile = typeDir </> named (typeFold t <> ".annah")+                let foldMorteFile = typeDir </> named (typeFold t)++                Filesystem.createDirectory True typeDir+                write typeAnnahFile (txt <> "in   " <> typeName t)+                let e0 = Family ts (Var (V (typeName t) 0))+                let typeTxt = Morte.pretty (Morte.normalize (Annah.desugar e0))+                write typeMorteFile typeTxt++                if typeFold t /= "_"+                    then do+                        write foldAnnahFile (txt <> "in   " <> typeFold t)+                        let e1 = Family ts (Var (V (typeFold t) 0))+                        let foldTxt =+                                Morte.pretty (Morte.normalize (Annah.desugar e1))+                        write foldMorteFile foldTxt+                    else return ()++                forM_ (typeDatas t) (\d -> do+                    let dataAnnahName = named (dataName d <> ".annah")+                    let dataMorteName = named (dataName d)+                    let dataAnnahFile = typeDir </> dataAnnahName+                    let dataMorteFile = typeDir </> dataMorteName++                    write dataAnnahFile (txt <> "in   " <> dataName d)++                    let e2 = Family ts (Var (V (dataName d) 0))+                    let dataTxt =+                            Morte.pretty (Morte.normalize (Annah.desugar e2))+                    write dataMorteFile dataTxt ) )

@@ -0,0 +1,594 @@+{-# LANGUAGE OverloadedStrings  #-}+{-# OPTIONS_GHC -Wall #-}++{-| This module contains the core machinery for the Annah language, which is a+    medium-level language that desugars to Morte.++    The main high-level features that Annah does not provide compared to Haskell+    are:++    * type classes++    * type inference++    You cannot type-check or normalize Annah expressions directly.  Instead,+    you `desugar` Annah expressions to Morte, and then type-check or normalize+    the Morte expressions using `M.typeOf` and `M.normalize`.++    Annah does everything through Morte for two reasons:++    * to ensure the soundness of type-checking and normalization, and:++    * to interoperate with other languages that compile to Morte.++    The typical workflow is:++    * You parse a `Text` source using `Annah.Parser.exprFromText`++    * You `desugar` the Annah expression to Morte++    * You resolve all imports using `M.load`++    * You type-check the Morte expression using `M.typeOf`++    * You `M.normalize` the Morte expression+-}++module Annah.Core (+    -- * Syntax+      M.Var(..)+    , M.Const(..)+    , Arg(..)+    , Let(..)+    , Data(..)+    , Type(..)+    , Bind(..)+    , Expr(..)++    -- * Desugaring+    , desugar+    , desugarFamily+    , desugarNatural+    , desugarDo+    , desugarList+    , desugarPath+    , desugarLets++    ) where++import Control.Applicative (pure, empty)+import Data.String (IsString(..))+import Data.Text.Lazy (Text)+import qualified Morte.Core as M+import Prelude hiding (pi)++{-| Argument for function or constructor definitions++> Arg "_" _A  ~       _A+> Arg  x  _A  ~  (x : _A)+-}+data Arg = Arg+    { argName :: Text+    , argType :: Expr+    } deriving (Show)++{-|+> Let f [a1, a2] _A rhs  ~  let f a1 a2 : _A = rhs+-}+data Let = Let+    { letName :: Text+    , letArgs :: [Arg]+    , letType :: Expr+    , letRhs  :: Expr+    } deriving (Show)++{-|+> Type t [d1, d2] f  ~  type t d1 d2 fold f+-}+data Type = Type+    { typeName  :: Text+    , typeDatas :: [Data]+    , typeFold  :: Text+    } deriving (Show)++{-|+> Data c [a1, a2]  ~  data c a1 a2+-}+data Data = Data+    { dataName :: Text+    , dataArgs :: [Arg]+    } deriving (Show)++{-|+> Bind arg e  ~  arg <- e;+-}+data Bind = Bind+    { bindLhs :: Arg+    , bindRhs :: Expr+    } deriving (Show)++-- | Syntax tree for expressions+data Expr+    -- | > Const c                         ~  c+    = Const M.Const+    -- | > Var (V x 0)                     ~  x+    --   > Var (V x n)                     ~  x@n+    | Var M.Var+    -- | > Lam x     _A  b                 ~  λ(x : _A) →  b+    | Lam Text Expr Expr+    -- | > Pi x      _A _B                 ~  ∀(x : _A) → _B+    | Pi  Text Expr Expr+    -- | > App f a                         ~  f a+    | App Expr Expr+    -- | > Annot a _A                      ~  a : _A+    | Annot Expr Expr+    -- | > Lets [l1, l2] e                 ~  l1 l2 in e+    | Lets [Let] Expr+    -- | > Family f e                      ~  f in e+    | Family [Type] Expr+    -- | > Natural n                       ~  n+    | Natural Integer+    -- | > List t [x, y, z]                ~  [nil t,x,y,z]+    | List Expr [Expr]+    -- | > Path c [(o1, m1), (o2, m2)] o3  ~  [id c {o1} m1 {o2} m2 {o3}]+    | Path Expr [(Expr, Expr)] Expr+    -- | > Do m [b1, b2] b3                ~  do m { b1 b2 b3 }+    | Do Expr [Bind] Bind+    | Embed M.Path+    deriving (Show)++instance IsString Expr where+    fromString str = Var (fromString str)++-- | Convert an Annah expression to a Morte expression+desugar+    :: Expr+    -- ^ Annah expression+    -> M.Expr M.Path+    -- ^ Morte expression+desugar (Const c     ) = M.Const c+desugar (Var v       ) = M.Var   v+desugar (Lam x _A  b ) = M.Lam x (desugar _A) (desugar  b)+desugar (Pi  x _A _B ) = M.Pi  x (desugar _A) (desugar _B)+desugar (App f a     ) = M.App (desugar f) (desugar a)+desugar (Embed  p    ) = M.Embed p+desugar (Annot a _A  ) = desugar (Lets [Let "x" [] _A a] "x")+desugar (Lets ls e   ) = desugarLets  ls               e+desugar (Family ts e ) = desugarLets (desugarFamily ts) e+desugar (Natural n   ) = desugarNatural n+desugar (List t es   ) = desugarList t es+desugar (Path t oms o) = desugarPath t oms o+desugar (Do m bs b   ) = desugarDo m bs b++{-| Convert a natural number to a Morte expression++    For example, this natural number:++> 4++    ... desugars to this Morte expression:++>     λ(Nat  : *                  )+> →   λ(Succ : ∀(pred : Nat) → Nat)+> →   λ(Zero : Nat                )+> →   Succ (Succ (Succ (Succ Zero)))+-}+desugarNatural :: Integer -> M.Expr M.Path+desugarNatural n0 =+    M.Lam "Nat" (M.Const M.Star)+        (M.Lam "Succ" (M.Pi "pred" (M.Var (M.V "Nat" 0)) (M.Var (M.V "Nat" 0)))+            (M.Lam "Zero" (M.Var (M.V "Nat" 0))+                (go0 n0) ) )+  where+    go0 n | n <= 0    = M.Var (M.V "Zero" 0)+          | otherwise = M.App (M.Var (M.V "Succ" 0)) (go0 (n - 1))++{-| Convert a list into a Morte expression++    For example, this list:++> [nil Bool, True, False, False]++    ... desugars to this Morte expression:++>     λ(List : *)+> →   λ(Cons : ∀(head : Bool) → ∀(tail : List) → List)+> →   λ(Nil : List)+> →   Cons True (Cons False (Cons False Nil))+-}+desugarList :: Expr -> [Expr] -> M.Expr M.Path+desugarList e0 ts0 =+    M.Lam "List" (M.Const M.Star)+        (M.Lam "Cons" (M.Pi "head" (desugar0 e0) (M.Pi "tail" "List" "List"))+            (M.Lam "Nil" "List" (go ts0)) )+  where+    go  []    = "Nil"+    go (t:ts) = M.App (M.App "Cons" (desugar1 t)) (go ts)++    desugar0 = M.shift 1 "List" . desugar++    desugar1 = M.shift 1 "List" . M.shift 1 "Cons" . M.shift 1 "Nil" . desugar++{-| Convert a path into a Morte expression++    For example, this path:++> [id cat {a} f {b} g {c}]++    ... desugars to this Morte expression:++>     λ(Path : ∀(a : *) → ∀(b : *) → *)+> →   λ(  Step+>     :   ∀(a : *)+>     →   ∀(b : *)+>     →   ∀(c : *)+>     →   ∀(head : cat a b)+>     →   ∀(tail : Path b c)+>     →   Path a c+>     )+> →   λ(End : ∀(a : *) → Path a a)+> →   Step a b c f (Step b c c g (End c))+-}+desugarPath+    ::  Expr+    ->  [(Expr, Expr)]+    ->  Expr+    ->  M.Expr M.Path+desugarPath c0 oms0 o0 =+    M.Lam "Path"+        (M.Pi "a" (M.Const M.Star) (M.Pi "b" (M.Const M.Star) (M.Const M.Star)))+        (M.Lam "Step"+            (M.Pi "a" (M.Const M.Star)+                (M.Pi "b" (M.Const M.Star)+                    (M.Pi "c" (M.Const M.Star)+                        (M.Pi "head" (M.App (M.App (desugar0 c0) "a") "b")+                            (M.Pi "tail" (M.App (M.App "Path" "b") "c")+                                (M.App (M.App "Path" "a") "c") ) ) ) ) )+            (M.Lam "End"+                (M.Pi "a" (M.Const M.Star) (M.App (M.App "Path" "a") "a"))+                (go oms0) ) )+  where+    desugar0+        =   M.shift 1 "Path"+        .   M.shift 1 "a"+        .   M.shift 1 "b"+        .   M.shift 1 "c"+        .   desugar+    desugar1+        =   M.shift 1 "Path"+        .   M.shift 1 "Step"+        .   M.shift 1 "End"+        .   desugar++    go []                         = M.App "End" (desugar1 o0)+    go [(o1, m1)]                 =+        M.App (M.App (M.App (M.App (M.App "Step" o1') o0') o0') m1') (go [] )+      where+        o0' = desugar1 o0+        o1' = desugar1 o1+        m1' = desugar1 m1+    go ((o1, m1):oms@((o2, _):_)) =+        M.App (M.App (M.App (M.App (M.App "Step" o1') o2') o0') m1') (go oms)+      where+        o0' = desugar1 o0+        o1' = desugar1 o1+        o2' = desugar1 o2+        m1' = desugar1 m1++{-| Convert a command (i.e. do-notation) into a Morte expression++    For example, this command:++> do m+> {   x0 : _A0 <- e0;+>     x1 : _A1 <- e1;+> }++    .. desugars to this Morte expression:++>     λ(Cmd : *)+> →   λ(Bind : ∀(b : *) → m b → (b → Cmd) → Cmd)+> →   λ(Pure : ∀(x1 : _A1) → Cmd)+> →   Bind _A0 e0+>     (   λ(x0 : _A0)+>     →   Bind _A1 e1+>         Pure+>     )+-}+desugarDo :: Expr -> [Bind] -> Bind -> M.Expr M.Path+desugarDo m bs0 (Bind (Arg x0 _A0) e0) =+    M.Lam "Cmd" (M.Const M.Star)+        (M.Lam "Bind"+            (M.Pi "b" (M.Const M.Star)+                (M.Pi "_" (M.App (desugar0 m) "b")+                    (M.Pi "_" (M.Pi "_" "b" "Cmd") "Cmd") ) )+            (M.Lam "Pure" (M.Pi x0 (desugar1 _A0) "Cmd")+                (go bs0 (0 :: Int) (0 :: Int)) ) )+  where+    desugar0+        = M.shift 1 "b"+        . M.shift 1 "Cmd"+        . desugar++    desugar1+        = M.shift 1 "Bind"+        . M.shift 1 "Cmd"+        . desugar++    desugar2+        = M.shift 1 "Pure"+        . M.shift 1 "Bind"+        . M.shift 1 "Cmd"+        . desugar++    go  []                    numPure numBind =+        M.App+            (M.App (M.App (M.Var (M.V "Bind" numBind)) (desugar2 _A0))+                (desugar2 e0) )+            (M.Var (M.V "Pure" numPure))+    go (Bind (Arg x _A) e:bs) numPure numBind = numBind' `seq` numPure' `seq`+        M.App+            (M.App+                (M.App (M.Var (M.V "Bind" numBind)) (desugar2 _A))+                (desugar2 e) )+            (M.Lam x (desugar2 _A) (go bs numBind' numPure'))+      where+        numBind' = if x == "Bind" then numBind + 1 else numBind+        numPure' = if x == "Pure" then numPure + 1 else numPure++{-| Convert a let expression into a Morte expression++    For example, this let expression:++> let f0 (x00 : _A00) ... (x0j : _A0j) _B0 = b0+> ..+> let fi (xi0 : _Ai0) ... (xij : _Aij) _Bi = bi+> in  e++    ... desugars to this Morte expression:++> (   \(f0 : forall (x00 : _A00) -> ... -> forall (x0j : _A0j) -> _B0)+> ->  ...+> ->  \(fi : forall (xi0 : _Ai0) -> ... -> forall (xij : _Aij) -> _Bi)+> ->  e+> )+>+> (\(x00 : _A00) -> ... -> \(x0j : _A0j) -> b0)+> ...+> (\(xi0 : _Ai0) -> ... -> \(xij : _Aij) -> bi)++-}+desugarLets :: [Let] -> Expr -> M.Expr M.Path+desugarLets lets e = apps+  where+    -- > (   \(f0 : forall (x00 : _A00) -> ... -> forall (x0j : _A0j) -> _B0)+    -- > ->  ...+    -- > ->  \(fi : forall (xi0 : _Ai0) -> ... -> forall (xij : _Aij) -> _Bi)+    -- > ->  e+    -- > )+    lams = foldr+        (\(Let fn args _Bn _) rest ->+            -- > forall (xn0 : _An0) -> ... -> forall (xnj : _Anj) -> _Bn+            let rhsType = pi args _Bn++            -- > \(fn : rhsType) -> rest+            in  M.Lam fn (desugar rhsType) rest )+        (desugar e)+        lets++    -- > lams+    -- > (\(x00 : _A00) -> ... -> \(x0j : _A0j) -> b0)+    -- > ...+    -- > (\(xi0 : _Ai0) -> ... -> \(xij : _Aij) -> bi)+    apps = foldr+        (\(Let _ args _ bn) rest ->+            -- > rest (\(xn0 : _An0) -> ... -> \(xnj : _Anj) -> bn)+            M.App rest (desugar (lam args bn)) )+        lams+        (reverse lets)++-- | A type or data constructor+data Cons = Cons+    { consName :: Text+    , consArgs :: [Arg]+    , consType :: Expr+    }++{-| This translates datatype definitions to let expressons using the+    Boehm-Berarducci encoding.++    For example, this mutually recursive datatype definition:++> type Even+> data Zero+> data SuccE (predE : Odd)+> fold foldEven+> +> type Odd+> data SuccO (predO : Even)+> fold foldOdd+> +> in SuccE++    ... desugars to seven let expressions:++> let Even : * = ...+> let Odd  : *+> let Zero : Even = ...+> let SuccE : ∀(predE : Odd ) → Even = ...+> let SuccO : ∀(predO : Even) → Odd  = ...+> let foldEven : ∀(x : Even) → ... = ...+> let foldOdd  : ∀(x : Odd ) → ... = ...+> in  SuccE++    ... and normalizes to:++>     λ(  predE+>     :   ∀(Even  : *)+>     →   ∀(Odd   : *)+>     →   ∀(Zero  : Even)+>     →   ∀(SuccE : ∀(predE : Odd ) → Even)+>     →   ∀(SuccO : ∀(predO : Even) → Odd)+>     →   Odd+>     )+> →   λ(Even : *)+> →   λ(Odd : *)+> →   λ(Zero : Even)+> →   λ(SuccE : ∀(predE : Odd) → Even)+> →   λ(SuccO : ∀(predO : Even) → Odd)+> →   SuccE (predE Even Odd Zero SuccE SuccO)++-}++desugarFamily :: [Type] -> [Let]+desugarFamily familyTypes = typeLets ++ dataLets ++ foldLets+{-  Annah permits data constructors to have duplicate names and Annah also+    permits data constructors to share the same name as type constructors.  A+    lot of the complexity of this code is due to avoiding name collisions.++    Constructor fields can also have duplicate field names, too.  This is+    particularly useful for constructors with multiple fields where the user+    omits the field name and defaults to @\"_\"@, like in this example:++    >     \(a : *)+    > ->  \(b : *)+    > ->  type Pair+    >     data MakePair a b+    >     in   MakePair++    ... which compiles to:++    >     \(a : *)+    > ->  \(b : *)+    > ->  \(_ : a)+    > ->  \(_ : b)+    > ->  \(Pair : *)+    > ->  \(MakePair : a -> b -> Pair)+    > ->  MakePair _@1 _+-}+  where+    typeConstructors :: [Cons]+    typeConstructors = do+        t <- familyTypes+        return (Cons (typeName t) [] (Const M.Star))++    dataConstructors :: [Cons]+    dataConstructors = do+        (tsBefore , t, tsAfter) <- zippers familyTypes+        (dsBefore1, d, _      ) <- zippers (typeDatas t)+        let dsBefore0 = do+                t' <- tsBefore+                typeDatas t'+        let names1  = map typeName tsAfter+        let names2  = map dataName dsBefore0+        let names3  = map dataName dsBefore1+        let names4  = map argName (dataArgs d)+        let typeVar =+                typeName t `isShadowedBy` (names1 ++ names2 ++ names3 ++ names4)+        return (Cons (dataName d) (dataArgs d) typeVar)++    constructors :: [Cons]+    constructors = typeConstructors ++ dataConstructors++    makeRhs piOrLam con = foldr cons con constructors+      where+        cons (Cons x args _A) = piOrLam x (pi args _A)++    typeLets, foldLets :: [Let]+    (typeLets, foldLets) = unzip (do+        let folds = map typeFold familyTypes+        ((_, t, tsAfter), fold) <- zip (zippers typeConstructors) folds+        let names1   = map consName tsAfter+        let names2   = map consName dataConstructors+        let con      = consName t `isShadowedBy` (names1 ++ names2)+        let typeRhs  = makeRhs Pi con+        let foldType = Pi  "x" con      typeRhs+        let foldRhs  = Lam "x" typeRhs  "x"+        return ( Let (consName t) [] (consType t) typeRhs+               , Let  fold        []  foldType    foldRhs+               ) )++    -- TODO: Enforce that argument types are `Var`s?+    desugarType :: Expr -> Maybe ([Arg], Expr, Expr)+    desugarType   (Pi x _A e      ) = do+        ~(args, f, f') <- desugarType e+        return (Arg x _A:args, f, f')+    desugarType f@(Var (M.V x0 n0)) = do+        f' <- go0 dataConstructors x0 n0+        return ([], f, f')+      where+        go0 (d:ds) x n | consName d == x =+            if n > 0 then go0 ds x $! n - 1 else empty+                       | otherwise       = go0 ds x n+        go0  []    x n                   = go1 (reverse typeLets) x n++        go1 (t:ts) x n | letName  t == x =+            if n > 0 then go1 ts x $! n - 1 else pure (letRhs t)+                       | otherwise       = go1 ts x n+        go1  []    _ _                   = empty+    desugarType _ = empty++    consVars :: [Text] -> [Expr]+    consVars argNames = do+        (_, name, namesAfter) <- zippers (map consName constructors)+        return (name `isShadowedBy` (argNames ++ namesAfter))++    dataLets :: [Let]+    dataLets = do+        (_, d, dsAfter) <- zippers dataConstructors+        let conVar  = consName d `isShadowedBy` map consName dsAfter+        let conArgs = do+                (_, arg, argsAfter) <- zippers (consArgs d)+                let names1 = map argName  argsAfter+                let names2 = map consName constructors+                return (case desugarType (argType arg) of+                    Nothing           -> argVar+                      where+                        names = names1 ++ names2+                        argVar = argName arg `isShadowedBy` names+                    Just (args, _, _) ->+                        lam args (apply argVar (argExprs ++ consVars names3))+                      where+                        names3 = map argName args+                        names = names1 ++ names2 ++ names3+                        argVar = argName arg `isShadowedBy` names+                        argExprs = do+                            (_, name, namesAfter) <- zippers names3+                            return (name `isShadowedBy` namesAfter) )+        let (lhsArgs, rhsArgs) = unzip (do+                arg@(Arg x _A) <- consArgs d+                return (case desugarType _A of+                    Just (args, _B, _B') -> (lhsArg, rhsArg)+                      where+                        lhsArg = Arg x (pi args _B )+                        rhsArg = Arg x (pi args _B')+                    Nothing              -> (   arg,    arg) ) )+        let letType' = pi  lhsArgs (consType d)+        let letRhs'  = lam rhsArgs (makeRhs Lam (apply conVar conArgs))+        return (Let (consName d) [] letType' letRhs')++-- | Apply an expression to a list of arguments+apply :: Expr -> [Expr] -> Expr+apply f as = foldr (flip App) f (reverse as)++{-| Compute the correct DeBruijn index for a synthetic `Var` (@x@) by providing+    all variables bound in between when @x@ is introduced and when @x@ is used.+-}+isShadowedBy :: Text -> [Text] -> Expr+x `isShadowedBy` vars = Var (M.V x (length (filter (== x) vars)))++pi, lam :: [Arg] -> Expr -> Expr+pi  args e = foldr (\(Arg x _A) -> Pi  x _A) e args+lam args e = foldr (\(Arg x _A) -> Lam x _A) e args++-- | > zippers [1, 2, 3] = [([], 1, [2, 3]), ([1], 2, [3]), ([2, 1], 3, [])]+zippers :: [a] -> [([a], a, [a])]+zippers  []           = []+zippers (stmt:stmts') = z:go z+  where+    z = ([], stmt, stmts')++    go ( _, _, []  ) = []+    go (ls, m, r:rs) = z':go z'+      where+        z' = (m:ls, r, rs)

@@ -0,0 +1,215 @@+{+{-# LANGUAGE OverloadedStrings #-}++-- | Lexing logic for the Annah language+module Annah.Lexer (+    -- * Lexer+    lexExpr,++    -- * Types+    Token(..),+    Position(..),+    LocatedToken(..)+    ) where++import Control.Monad.Trans.State.Strict (State)+import Data.Bits (shiftR, (.&.))+import Data.Char (ord, digitToInt, isDigit)+import Data.Int (Int64)+import Data.Text.Lazy (Text)+import Data.Word (Word8)+import Filesystem.Path.CurrentOS (FilePath, fromText)+import Lens.Family.State.Strict ((.=), (+=))+import Pipes (Producer, for, lift, yield)+import Prelude hiding (FilePath)++import qualified Control.Monad.Trans.State.Strict as State+import qualified Data.Text.Lazy                   as Text++}++$digit = 0-9++-- Same as Haskell+$opchar = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~]++$fst   = [A-Za-z_]+$label = [A-Za-z0-9_]++$nonwhite       = ~$white+$whiteNoNewline = $white # \n++$path = [$label \\\/\.]++tokens :-++    $whiteNoNewline+                  ;+    \n                              { \_    -> lift (do+                                        line   += 1+                                        column .= 0 )                          }+    "--".*                          ;+    "("                             { \_    -> yield OpenParen                 }+    ")"                             { \_    -> yield CloseParen                }+    "{"                             { \_    -> yield OpenBrace                 }+    "}"                             { \_    -> yield CloseBrace                }+    "[nil"                          { \_    -> yield OpenList                  }+    "[id"                           { \_    -> yield OpenPath                  }+    "]"                             { \_    -> yield CloseBracket              }+    ","                             { \_    -> yield Comma                     }+    ":"                             { \_    -> yield Colon                     }+    ";"                             { \_    -> yield Semicolon                 }+    "@"                             { \_    -> yield At                        }+    "*"                             { \_    -> yield Star                      }+    "BOX" | "□"                     { \_    -> yield Box                       }+    "->" | "→"                      { \_    -> yield Arrow                     }+    "<-" | "←"                      { \_    -> yield LArrow                    }+    "\/" | "|~|" | "forall" | "∀" | "Π" { \_ -> yield Pi                       }+    "\" | "λ"                       { \_    -> yield Lambda                    }+    "type"                          { \_    -> yield Type                      }+    "fold"                          { \_    -> yield Fold                      }+    "data"                          { \_    -> yield Data                      }+    "let"                           { \_    -> yield Let                       }+    "="                             { \_    -> yield Equals                    }+    "in"                            { \_    -> yield In                        }+    "do"                            { \_    -> yield Do                        }+    $digit+                         { \text -> yield (Number (toInt text))     }+    $fst $label* | "(" $opchar+ ")" { \text -> yield (Label text)              }+    "https://" $nonwhite+           { \text -> yield (URL text)                }+    "http://" $nonwhite+            { \text -> yield (URL text)                }+    "/" $nonwhite+                  { \text -> yield (File (toFile 0 text))    }+    "./" $nonwhite+                 { \text -> yield (File (toFile 2 text))    }+    "../" $nonwhite+                { \text -> yield (File (toFile 0 text))    }++{+toInt :: Text -> Int+toInt = Text.foldl' (\x c -> 10 * x + digitToInt c) 0++toFile :: Int64 -> Text -> FilePath+toFile n = fromText . Text.toStrict . Text.drop n++trim :: Text -> Text+trim = Text.init . Text.tail++-- This was lifted almost intact from the @alex@ source code+encode :: Char -> (Word8, [Word8])+encode c = (fromIntegral h, map fromIntegral t)+  where+    (h, t) = go (ord c)++    go n+        | n <= 0x7f   = (n, [])+        | n <= 0x7ff  = (0xc0 + (n `shiftR` 6), [0x80 + n .&. 0x3f])+        | n <= 0xffff =+            (   0xe0 + (n `shiftR` 12)+            ,   [   0x80 + ((n `shiftR` 6) .&. 0x3f)+                ,   0x80 + n .&. 0x3f+                ]+            )+        | otherwise   =+            (   0xf0 + (n `shiftR` 18)+            ,   [   0x80 + ((n `shiftR` 12) .&. 0x3f)+                ,   0x80 + ((n `shiftR` 6) .&. 0x3f)+                ,   0x80 + n .&. 0x3f+                ]+            )++-- | The cursor's location while lexing the text+data Position = P+    { lineNo    :: {-# UNPACK #-} !Int+    , columnNo  :: {-# UNPACK #-} !Int+    } deriving (Show)++-- line :: Lens' Position Int+line :: Functor f => (Int -> f Int) -> Position -> f Position+line k (P l c) = fmap (\l' -> P l' c) (k l)++-- column :: Lens' Position Int+column :: Functor f => (Int -> f Int) -> Position -> f Position+column k (P l c) = fmap (\c' -> P l c') (k c)++{- @alex@ does not provide a `Text` wrapper, so the following code just modifies+   the code from their @basic@ wrapper to work with `Text`++   I could not get the @basic-bytestring@ wrapper to work; it does not correctly+   recognize Unicode regular expressions.+-}+data AlexInput = AlexInput+    { prevChar  :: Char+    , currBytes :: [Word8]+    , currInput :: Text+    }++alexGetByte :: AlexInput -> Maybe (Word8,AlexInput)+alexGetByte (AlexInput c bytes text) = case bytes of+    b:ytes -> Just (b, AlexInput c ytes text)+    []     -> case Text.uncons text of+        Nothing       -> Nothing+        Just (t, ext) -> case encode t of+            (b, ytes) -> Just (b, AlexInput t ytes ext)++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar = prevChar++{-| 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)+lexExpr text = for (go (AlexInput '\n' [] text)) tag+  where+    tag token = do+        pos <- lift State.get+        yield (LocatedToken token pos)++    go input = case alexScan input 0 of+        AlexEOF                        -> return Nothing+        AlexError (AlexInput _ _ text) -> return (Just text)+        AlexSkip  input' len           -> do+            lift (column += len)+            go input'+        AlexToken input' len act       -> do+            act (Text.take (fromIntegral len) (currInput input))+            lift (column += len)+            go input'++-- | A `Token` augmented with `Position` information+data LocatedToken = LocatedToken+    { token    ::                !Token+    , position :: {-# UNPACK #-} !Position+    } deriving (Show)++-- | Token type, used to communicate between the lexer and parser+data Token+    = OpenParen+    | CloseParen+    | OpenBrace+    | CloseBrace+    | OpenList+    | OpenPath+    | CloseBracket+    | Period+    | Comma+    | Colon+    | Semicolon+    | At+    | Star+    | Box+    | Arrow+    | LArrow+    | Lambda+    | Pi+    | Type+    | Fold+    | Data+    | Let+    | Equals+    | In+    | Do+    | Label Text+    | Number Int+    | File FilePath+    | URL Text+    | EOF+    deriving (Eq, Show)+}

@@ -0,0 +1,260 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE OverloadedStrings  #-}+{-# LANGUAGE RankNTypes         #-}+{-# LANGUAGE RecursiveDo        #-}++-- | Parsing logic for the Morte language++module Annah.Parser (+    -- * Parser+    exprFromText,+    typesFromText,++    -- * Errors+    ParseError(..),+    ParseMessage(..)+    ) where++import Annah.Core+import Annah.Lexer (Position, Token, LocatedToken(..))+import Control.Applicative hiding (Const)+import Control.Exception (Exception)+import Control.Monad.Trans.Class  (lift)+import Control.Monad.Trans.Except (Except, throwE, runExceptT)+import Control.Monad.Trans.State.Strict (evalState, get)+import Data.Monoid+import Data.Text.Buildable (Buildable(..))+import Data.Text.Lazy (Text)+import Data.Text.Lazy.Builder (toLazyText)+import Data.Typeable (Typeable)+import Morte.Core (Path(..))+import Filesystem.Path.CurrentOS (FilePath)+import Prelude hiding (FilePath)+import Text.Earley++import qualified Annah.Lexer    as Lexer+import qualified Pipes.Prelude  as Pipes+import qualified Data.Text.Lazy as Text++match :: Token -> Prod r Token LocatedToken Token+match t = fmap Lexer.token (satisfy predicate) <?> t+  where+    predicate (LocatedToken t' _) = t == t'++label :: Prod r e LocatedToken Text+label = fmap unsafeFromLabel (satisfy isLabel)+  where+    isLabel (LocatedToken (Lexer.Label _) _) = True+    isLabel  _                               = False++    unsafeFromLabel (LocatedToken (Lexer.Label l) _) = l++number :: Prod r e LocatedToken Int+number = fmap unsafeFromNumber (satisfy isNumber)+  where+    isNumber (LocatedToken (Lexer.Number _) _) = True+    isNumber  _                                = False++    unsafeFromNumber (LocatedToken (Lexer.Number n) _) = n++file :: Prod r e LocatedToken FilePath+file = fmap unsafeFromFile (satisfy isFile)+  where+    isFile (LocatedToken (Lexer.File _) _) = True+    isFile  _                              = False++    unsafeFromFile (LocatedToken (Lexer.File n) _) = n++url :: Prod r e LocatedToken Text+url = fmap unsafeFromURL (satisfy isURL)+  where+    isURL (LocatedToken (Lexer.URL _) _) = True+    isURL  _                             = False++    unsafeFromURL (LocatedToken (Lexer.URL n) _) = n++sepBy1 :: Alternative f => f a -> f b -> f [a]+sepBy1 x sep = (:) <$> x <*> many (sep *> x)++sepBy :: Alternative f => f a -> f b -> f [a]+sepBy x sep = sepBy1 x sep <|> pure []++expr+    :: Grammar r+        (Prod r Token LocatedToken Expr, Prod r Token LocatedToken [Type])+expr = mdo+    expr0 <- rule+        (   Annot <$> expr1 <*> (match Lexer.Colon *> expr0)+        <|> expr1+        )+    expr1 <- rule+        (       Lam+            <$> (match Lexer.Lambda *> match Lexer.OpenParen *> label)+            <*> (match Lexer.Colon *> expr1)+            <*> (match Lexer.CloseParen *> match Lexer.Arrow *> expr1)+        <|>     Pi+            <$> (match Lexer.Pi *> match Lexer.OpenParen *> label)+            <*> (match Lexer.Colon *> expr1)+            <*> (match Lexer.CloseParen *> match Lexer.Arrow *> expr1)+        <|> Pi "_" <$> expr2 <*> (match Lexer.Arrow *> expr1)+        <|> Family <$> types <*> (match Lexer.In *> expr1)+        <|> Lets <$> lets <*> (match Lexer.In *> expr1)+        <|> expr2+        )++    vexpr <- rule+        (   V <$> label <*> (match Lexer.At *> number)+        <|> V <$> label <*> pure 0+        )++    expr2 <- rule+        (   App <$> expr2 <*> expr3+        <|> expr3+        )++    let makeExpr3 p =+            (   Var <$> vexpr+            <|> match Lexer.Star *> pure (Const Star)+            <|> match Lexer.Box  *> pure (Const Box )+            <|> Embed <$> embed+            <|> (Natural . fromIntegral) <$> number+            <|>     List+                <$> (match Lexer.OpenList *> expr0)+                <*> (many (match Lexer.Comma *> expr0) <* match Lexer.CloseBracket)+            <|>     Path+                <$> (match Lexer.OpenPath *> expr0)+                <*> many ((,) <$> object <*> expr0)+                <*> (object <* match Lexer.CloseBracket)+            <|>     Do+                <$> (match Lexer.Do *> expr0)+                <*> (match Lexer.OpenBrace *> many bind)+                <*> (bind <* match Lexer.CloseBrace)+            <|> (match Lexer.OpenParen *> p <* match Lexer.CloseParen)+            )++    expr3  <- rule (makeExpr3 expr0)+    expr3' <- rule (makeExpr3 expr1)++    arg <- rule+        (       Arg+            <$> (match Lexer.OpenParen *> label)+            <*> (match Lexer.Colon *> expr1 <* match Lexer.CloseParen)+        <|>     Arg "_" <$> expr3'+        )++    args <- rule (many arg)++    data_ <- rule (Data <$> (match Lexer.Data *> label) <*> args)++    datas <- rule (many data_)++    type_ <- rule+        (       Type+            <$> (match Lexer.Type *> label)+            <*> datas+            <*> (match Lexer.Fold *> label)+        <|>     Type+            <$> (match Lexer.Type *> label)+            <*> datas+            <*> pure "_"+        )++    types <- rule (some type_)++    let_ <- rule+        (   Let+        <$> (match Lexer.Let *> label)+        <*> args+        <*> (match Lexer.Colon *> expr0)+        <*> (match Lexer.Equals *> expr1)+        )++    lets <- rule (some let_)++    object <- rule (match Lexer.OpenBrace *> expr0 <* match Lexer.CloseBrace)++    bind <- rule+        (   (\x y z -> Bind (Arg x y) z)+        <$> label+        <*> (match Lexer.Colon *> expr0)+        <*> (match Lexer.LArrow *> expr0 <* match Lexer.Semicolon)+        )++    embed <- rule+        (   File <$> file+        <|> URL <$> url+        )++    return (expr0, types)++-- | The specific parsing error+data ParseMessage+    -- | Lexing failed, returning the remainder of the text+    = Lexing Text+    -- | Parsing failed, returning the invalid token and the expected tokens+    | Parsing Token [Token]+    deriving (Show)++-- | Structured type for parsing errors+data ParseError = ParseError+    { position     :: Position+    , parseMessage :: ParseMessage+    } deriving (Typeable)++instance Show ParseError where+    show = Text.unpack . toLazyText . build++instance Exception ParseError++instance Buildable ParseError where+    build (ParseError (Lexer.P l c) e) =+            "\n"+        <>  "Line:   " <> build l <> "\n"+        <>  "Column: " <> build c <> "\n"+        <>  "\n"+        <>  case e of+            Lexing r                                     ->+                    "Lexing: \"" <> build remainder <> dots <> "\"\n"+                <>  "\n"+                <>  "Error: Lexing failed\n"+              where+                remainder = Text.takeWhile (/= '\n') (Text.take 64 r)+                dots      = if Text.length r > 64 then "..." else mempty+            Parsing t ts ->+                    "Parsing : " <> build (show t ) <> "\n"+                <>  "Expected: " <> build (show ts) <> "\n"+                <>  "\n"+                <>  "Error: Parsing failed\n"++runParser+    :: (forall r . Grammar r (Prod r Token LocatedToken a))+    -> Text+    -> Either ParseError a+runParser p text = evalState (runExceptT m) (Lexer.P 1 0)+  where+    m = do+        (locatedTokens, mtxt) <- lift (Pipes.toListM' (Lexer.lexExpr text))+        case mtxt of+            Nothing  -> return ()+            Just txt -> do+                pos <- lift get+                throwE (ParseError pos (Lexing txt))+        let (parses, Report _ needed found) =+                fullParses (parser p) locatedTokens+        case parses of+            parse:_ -> return parse+            []      -> do+                let LocatedToken t pos = case found of+                        lt:_ -> lt+                        _    -> LocatedToken Lexer.EOF (Lexer.P 0 0)+                throwE (ParseError pos (Parsing t needed))++-- | Parse an `Expr` from `Text` or return a `ParseError` if parsing fails+exprFromText :: Text -> Either ParseError Expr+exprFromText = runParser (fmap fst expr)++{-| Parse a type definition from `Text` or return a `ParseError` if parsing+    fails+-}+typesFromText :: Text -> Either ParseError [Type]+typesFromText = runParser (fmap snd expr)

@@ -0,0 +1,1699 @@+{-| Annah is a tiny language that serves to illustrate how various programming+    constructs can be desugared to lambda calculus.  The most sophisticated+    feature that Annah supports is desugaring mutually recursive datatypes+    to non-recursive lambda expressions.++    Annah is not intended to be used as a production language.  Rather, Annah is+    a step along the way towards a production language that I factored out as+    a reusable library that others can learn from and possibly fork for their+    own use cases.++    Under the hood, all Annah expressions are translated to a minimalist+    implementation of the calculus of constructions called Morte, which only+    supports non-recursive lambda expressions and their types.  You can find+    the Morte compiler and library here:++    <http://hackage.haskell.org/package/morte>++    Annah piggybacks on Morte meaning all Annah expressions are translated to+    Morte expressions and then those Morte expressions are type-checked and+    evaluated.  You cannot directly type-check or evaluate Annah expressions;+    you have to desugar them to Morte expressions first before you can do+    anything else with them.++    Annah is not very user-friendly (and I apologize for that!).  For example,+    Annah reuses Morte's type-checker which means that error messages are in+    terms of low-level lambda calculus expressions and not in terms of the+    original Annah source code.+  +    Most notably, Annah does not provide support for text, due to the gross+    inefficiency of encoding even basic ASCII text in lambda calculus.  Text+    handling would be better served by a backend with primitive support for+    text literals and operations on text.++    This tutorial assumes that you have first read the Morte tutorial, which+    you can find here:++    <http://hackage.haskell.org/package/morte/docs/Morte-Tutorial.html>++    Annah is a superset of Morte that implements many of the higher-level+    constructs mentioned in the Morte tutorial, which is why you should not skip+    reading the Morte tutorial.+-}++module Annah.Tutorial (+    -- * Introduction+    -- $introduction++    -- * Let+    -- $let++    -- * Data types+    -- $datatypes++    -- * Imports+    -- $imports++    -- * Autogenerate Types+    -- $types++    -- * Folds+    -- $folds++    -- * Recursive types+    -- $recursive++    -- * Prelude+    -- $prelude++    -- * Natural numbers+    -- $nats++    -- * Lists+    -- $lists++    -- * Monoids+    -- $monoids++    -- * Commands+    -- $commands++    -- * IO+    -- $io++    -- * Paths+    -- $paths++    -- * Conclusion+    -- $conclusion+    ) where++{- $introduction+    This library comes with a binary executable that you can use to compile+    Annah expressions to Morte expressions.  This executable can be used in two+    separate ways.++    First, you can read an Annah expression from standard input and the program+    will output the equivalent low-level Morte expression to standard output:++> $ annah+> type Bool+> data True+> data False+> fold if+> in                                                   +>     +> let not (b : Bool) : Bool = if b Bool False True+> in  not False+> <Ctrl-D>+> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++    Second, you can read an Annah expression in from a file if you provide the+    file name on the command line using the @compile@ subcommand:++> $ cat example.annah+> type Bool+> data True+> data False+> fold if+> in                                                   +>     +> let not (b : Bool) : Bool = if b Bool False True+> in  not False++> $ annah compile example.annah+> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++    Annah is a superset of Morte, so any Morte expression is also a valid Annah+    expression:++> $ annah+> \(a : *) -> \(x : a) -> x+> <Ctrl-D>+> λ(a : *) → λ(x : a) → x++    Like Morte, Annah is an explicitly typed language (i.e. no type inference).+-}++{- $let+    Annah supports let expressions which can be used to introduce functions and+    values.  For example, this is how you can define the polymorphic identity+    function in Annah:++> $ annah+> let id (a : *) (x : a) : a = x+> in  id+> <Ctrl-D>+> λ(a : *) → λ(x : a) → x++    You can define more than one thing in a let expression as long as you+    prefix each definition with @let@:++> $ annah+> let id (a : *) (x : a) : a = x  +> let const (a : *) (b : *) (x : a) (y : b) : a = x+> in  id+> <Ctrl-D>+> λ(a : *) → λ(x : a) → x++    The general form of a @let@ expression is:++> let f0 (x00 : _A00) (x01 : _A01) ... (x0j : _A0j) _B0 = b0+> let f1 (x10 : _A10) (x11 : _A11) ... (x1j : _A1j) _B1 = b1+> ...+> let fi (xi0 : _Ai0) (xi1 : _Ai1) ... (xij : _Aij) _Bi = bi+> in  e++    The above let expression desugars to the following lambda expression:++> (   λ(f0 : ∀(x00 : _A00) → ∀(x01 : _A01) → ... → ∀(x0j : _A0j) → _B0)+> →   λ(f1 : ∀(x10 : _A10) → ∀(x11 : _A11) → ... → ∀(x1j : _A1j) → _B1)+> →   ...+> →   λ(fi : ∀(xi0 : _Ai0) → ∀(xi1 : _Ai1) → ... → ∀(xij : _Aij) → _Bi)+> →   e+> )+> +> (λ(x00 : _A00) → λ(x01 : _A01) → ... → λ(x0j : _A0j) → b0)+> (λ(x10 : _A10) → λ(x11 : _A11) → ... → λ(x1j : _A1j) → b1)+> ...+> (λ(xi0 : _Ai0) → λ(xi1 : _Ai1) → ... → λ(xij : _Aij) → bi)++    The above @\'e\'@  is the \"body\" of the let expression and @f0@ through+    @fi@ are the \"let-bound terms\".  Due to the above translation, each+    \"let-bound\" term is only in scope for the \"body\" of the let-expression+    and the types of subsequent \"let-bound\" terms.++    To give a concrete example, our original @id@+@const@ let expression:++> let id (a : *) (x : a) : a = x  +> let const (a : *) (b : *) (x : a) (y : b) : a = x+> in  id++    ... was equivalent to:++> (   λ(id : ∀(a : *) → ∀(x : a) → a)+> →   λ(const : ∀(a : *) → ∀(b : *) → ∀(x : a) → ∀(y : b) → a+> →   id+> )+>+> (λ(a : *) → λ(x : a) → x)+> (λ(a : *) → λ(b : *) → λ(x : a) → λ(y : b) → x)++    ... which normalizes to:++> λ(a : *) → λ(x : a) → x++    The definition of @const@ is dead code that is optimized away by β-reduction+    because the let-bound @const@ term is never used within the body of the let+    expression.+-}++{- $datatypes+    Annah lets you define datatypes that scope over an expression.  For example,+    if you write:++> type Bool+> data True+> data False+> fold if+> in e++    ... then within the expression @\'e\'@ you will be able to use the @Bool@+    type, the @True@ and @False@ values, and the @if@ fold.++    The above definition of @Bool@ desugars to the following @let@ expression:++> let Bool  : *    = ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> let True  : Bool = λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True+> let False : Bool = λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False+> let if : Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool =+>     λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x+> in  e++    ... which in turn desugars to:++> (   λ(Bool : *)+> →   λ(True : Bool)+> →   λ(False : Bool)+> →   λ(if : Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)+> →   e+> )+> +> (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)+> (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True)+> (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False)+> (λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x)++    Annah also supports recursive datatypes.  For example, you can define+    natural numbers like this:++> $ annah+> type Nat+> data Succ (pred : Nat)+> data Zero+> in   Succ (Succ (Succ Zero))+> <Ctrl-D>+> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))++    Notice how we can omit the @fold@ line, which is optional.++    You can also omit field names, too, and this code is also valid:++> $ annah+> type Nat+> data Succ Nat+> data Zero+> in   Succ (Succ (Succ Zero))+> λ(Nat : *) → λ(Succ : Nat → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))++    Field names are just used to give nicer names to bound variables in the+    desugared datatype definition and field names default to @\'_\'@ if you omit+    the name.++    You can find out how any given type or constructor is encoded by just+    returning the constructor as the result of the let expression:++> $ annah+> type Nat+> data Succ (pred : Nat)+> data Zero+> in   Succ+> λ(pred : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (pred Nat Succ Zero)++-}++{- $imports+    Annah supports imports using the same syntax as Morte but you may only+    import Morte expressions (/not/ Annah expressions).  You can embed a file+    path or http URL anywhere within an expression and Annah will substitute in+    the Morte expression (encoded as plain text) located at that path or URL.++    The reason Annah does not support importing Annah expressions is that Annah+    does not actually resolve the imports.  Annah piggybacks off of Morte's+    support for imports, and Morte only supports importing Morte expressions.++    Imports are extremely useful when combined with datatypes because you can+    create a separate file for each type and constructor of a datatype.  To+    illustrate this we'll manually encode @Bool@, @True@, @False@, and @if@ as+    separate Annah files (and later we will see how we can auto-generate these+    files):++> $ cat Bool.annah+> type Bool+> data True+> data False+> fold if+> in   Bool++> $ cat True.annah+> type Bool+> data True+> data False+> fold if+> in   True++> $ cat False.annah+> type Bool+> data True+> data False+> fold if+> in   False++> $ cat if.annah+> type Bool+> data True+> data False+> fold if+> in   if++    Then we will translate each of them to a file encoding the equivalent Morte+    expression without the @\".annah\"@ file suffix:++> $ annah compile  Bool.annah >  Bool+> $ annah compile  True.annah >  True+> $ annah compile False.annah > False+> $ annah compile    if.annah >    if++    Now that we've created a file for each type and term we can import them+    within other expressions.  For example, now we can define the @not@ function+    in terms of imported types and values:++> $ cat not.annah+> let not (b : ./Bool ) : ./Bool = ./if b ./Bool ./False ./True+> in  not++    Don't worry if you don't understand what the above expression means just+    yet.  This tutorial will explain what the right-hand side means in the+    section on \"Folds\".++    We can run this file through Annah, which will desugar and normalize the+    expression, but will preserve the original imports:++> $ annah compile not.annah > not+> $ cat not+> λ(b : ./Bool ) → ./if  b ./Bool  ./False  ./True++    Annah actually does resolve the imports for the purposes of type-checking+    the expression, but deliberately does not resolve the imports for the final+    normalized expression.  Annah does this to keep the expression \"dynamically+    linked\" so that the expression can continue to reflect changes to+    dependencies.++    If you prefer to statically link the expression then you can use Morte:++> $ echo "./not" | morte+> ∀(b : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(b : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → b (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True)++    ... and you can also expand derived expressions, too:++> $ morte+> ./not ./True+> <Ctrl-D>+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False++    ... desugaring them with Annah if necessary:++> $ annah | morte+> let doubleNegate (b : ./Bool ) : /Bool = ./not (./not b)+> in  doubleNegate ./True+> <Ctrl-D>+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+>+> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++-}++{- $types+    Creating one file per type, fold, and data constructor gets tedious pretty+    quickly, so the @annah@ executable provides a convenient subcommand named+    @types@ for auto-generating these files.++    Just run the @annah types@ command and provide a datatype definition on+    standard input:++> $ annah types+> type Bool+> data True+> data False+> fold if+> <Ctrl-D>++    ... and @annah@ will create one directory for each type in the datatype+    definition:++> $ ls+> Bool/  Bool.annah++    Each type's directory will have two files per data constructor associated+    with the type and two files for the @fold@, too:++> $ ls Bool+> @  False  False.annah  if  if.annah  True  True.annah++    Everything comes in two flavors: the original Annah code and the equivalent+    Morte code:++> $ cat Bool/True.annah +> type Bool+> data True+> data False+> fold if+> in   True+> $ cat Bool/True+> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++    The Morte code for the type is located as a file named @\@@ underneath the+    type's directory:++> $ cat Bool.annah+> type Bool+> data True+> data False+> fold if+> in   Bool+> $ cat Bool/@+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool++    This is because Morte supports importing the directory by name if there is a+    file named @\@@ underneath the directory.  So, for example if you import+    @./Bool@ and it's a directory then Morte will import @.\/Bool\/\@@ instead:++> $ morte+> ./Bool+> <Ctrl-D>+> *+> +> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+-}++{- $folds+    Every datatype definition comes with an optional @fold@ which you can use to+    pattern match on a value of that type.  You can see what arguments the+    pattern match expects just by querying the type of the fold:++> $ morte+> ./Bool/if+> <Ctrl-D>+> ∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x++    ... and we can use imports to simplify the type to:++> ∀(x : ./Bool ) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool++    This type says that @if@ expects the following arguments:++    * A value named @x@ of type @./Bool@ to pattern match on (like+      @.\/Bool\/True@ or @.\/Bool\/False@)+    * The type of the result for each branch of the pattern match+    * The result to return if our value equals @.\/Bool\/True@+    * The result to return if our value equals @.\/Bool\/False@++    Carefully note that the second argument is named @Bool@ but can actually be+    any type.  Similarly, the third and fourth arguments are named after the+    @True@ and @False@ constructors but they actually represent how to handle+    each branch of the pattern match.++    So, for example, when we write:++> let not (b : ./Bool ) : ./Bool = ./if b ./Bool ./False ./True+> in  not++    ... it's as if we wrote the following Haskell code using pattern matching:++> let not :: Bool -> Bool+>     not b = case b of+>             True  -> False+>             False -> True+> in  not++    We could even format our code to parallel the layout of a Haskell pattern+    match:++> let not (b : ./Bool ) : ./Bool =+>     ./if b ./Bool+>     ./False+>     ./True+> in  not++    The only difference is that in the Annah code we have to explicitly supply+    the expected type of the result after the value that we pattern match on+    (i.e. the @./Bool@ immediately after the @./if b@).++    Our @./not@ function technically did not need to use the @./if@ @fold@.  For+    example, we could instead write:++> $ cat not.annah+> let not (b : ./Bool ) : ./Bool = b ./Bool ./False ./True+> in  not++    The @./if@ was unnecessary because it was just the identity function on+    @./Bool@s:++> $ cat if+> λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x++    .. which is the same as:++> λ(x : ./Bool ) → x++    The reason we can omit the @if@ is that all values of type @./Bool@ are+    already preformed pattern matches.  We can prove this to ourselves by+    consulting the definitions of @.\/Bool\/True@ and @.\/Bool\/False@:++> $ morte < ./Bool/True+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True+> $ morte < ./Bool/False+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False++    In other words, @.\/Bool\/True@ is just a preformed pattern match that+    always returns the first branch that you supply.  Vice versa,+    @.\/Bool\/False@ is just a preformed pattern match that always returns the+    second branch that you supply.++    In fact, all @fold@s are optional when you save a type and associated data+    constructors as separate files.  The only time we truly require the @fold@+    is when we pattern match on the type within the "body" of a datatype+    expression, like in our very first example:++> type Bool+> data True+> data False+> fold if+> in -- Everything below here is the "body" of the `Bool` datatype definition+>+> let not (b : Bool) : Bool = if b Bool False True+> in  not False++    @Bool@ and @./Bool@ are not the same type within the "body" of the @Bool@+    datatype definition.  If you omit the @if@ then you will get the following+    type error:++> $ annah+> type Bool+> data True+> data False+> fold if+> in+> +> let not (b : Bool) : Bool = b Bool False True+> in  not False+> <Ctrl-D>+> annah: +> Context:+> Bool : *+> True : Bool+> False : Bool+> if : ∀(x : Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> b : Bool+> +> Expression: b Bool+> +> Error: Only functions may be applied to values++    The @Context@ the compiler prints in the error message shows that the+    type-checker views the @Bool@ type as abstract and not the type of a+    pattern match.  However, the same @Context@ says that @if@ has the correct+    type to convert between the abstract @Bool@ type and the type we expect for+    a pattern match:++> if : ∀(x : Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool++    ... which we can simplify to just:++> -- The type of the bound variable named `if`+> if : ∀(x : Bool) → ./Bool++    In other words, @Bool@ and @./Bool@ are different types from the type+    checker's point of view.  That is why you must explicitly convert from+    @Bool@ to @./Bool@ using @if@ while inside that context.++    However, once you save @./Bool@, @./True@, @./False@ and @./if@ to separate+    files the distinction between @Bool@ and @./Bool@ vanishes.  The type of+    @./if@ (the file) is not the same as the type of @if@ (the bound variable):++> -- The type of the file named `./if`+> ./if : ∀(x : ./Bool ) → ./Bool++    You can deduce why the distinction disappears when you save things to+    separate files if you desugar the datatype definitions.  For example our+    @if.annah@ file was defined as:++> type Bool+> data True+> data False+> fold if+> in   if++    We can use the @annah desugar@ subcommand to see what that code desugars to+    before normalization:++> $ annah desugar < ./Bool/if.annah+> (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → λ(if : ∀(x : Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → if) (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False) (λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x)++    ... which we can clean up a bit to get:++> (   λ(Bool : *)+> →   λ(True : Bool)+> →   λ(False : Bool)+> →   λ(if : Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)+> →   if+> )+> +> (∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool)+> (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True)+> (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False)+> (λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x)++    That then normalizes to;++> $ annah desugar < ./Bool/if.annah | morte+> ∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x++    There is also another use for storing @fold@s as files and using them, even+    if they are not immediately necessary.  Saving a @fold@ to a file lets you+    provide a stable interface for pattern matching on a value if you ever+    want to change the internal implementation of a type without breaking+    backwards compatibility.++    For example, suppose that a user writes the following @not@ function using+    @./if@:++> let not (b : ./Bool ) : ./Bool = ./if b ./Bool ./False ./True+> in  not++    ... but we later decide we want to flip the order of of the @True@ and+    @False@ constructors in our datatype definition:++> $ annah types+> type Bool+> data False+> data True++    The above changes would break the user's code unless we change @./if@ to+    export the pattern match order that the user expects:++> $ cat > if+>     \(b : ./Bool )+> ->  \(Bool : *)+> ->  \(True : Bool)+> ->  \(False : Bool)+> ->  b Bool False True+> <Ctrl-D>++    Now the user's code continues to work as if nothing ever happened.++    So saving @fold@s to files and using them to pattern match is not strictly+    necessary, but if you do use them then you can change the underlying+    implementation of the type without breaking backwards compatibility.++    There's no way that you can force users to use the @fold@ that you provide+    since all saved expressions are encoded in lambda calculus, which does not+    provide any support for implementation hiding or encapsulation.  The best+    you can do is to simply warn users that you might break their code some+    day if they perform a \"raw pattern match\" (i.e. a pattern match without+    the use of a saved @fold@).+-}++{- $recursive+    Annah supports recursive and mutually recursive types.  We saw an example+    of recursive types with natural numbers:++> $ annah+> type Nat+> data Succ (pred : Nat)+> data Zero+> fold foldNat+>+> in   Succ (Succ (Succ Zero))+> <Ctrl-D>+> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))++    What might not be obvious is that if you save each type and constructor to+    a separate file then you can build a natural number just from the files.++    To illustrate this, we will compile our datatype definition to separate+    files:++> $ annah types+> type Nat+> data Succ (pred : Nat)+> data Zero+> fold foldNat+> <Ctrl-D>++    ... and now we can build natural numbers using these files:++> $ morte+> ./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))++    This gives the exact same result as before, but now we are programming+    directly at the "top level" using files instead of programming inside the+    body of a datatype definition.++    We can also fold natural numbers using our @.\/Nat\/foldNat@ function.+    Let's consult the type of the function:++> ∀(x : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(x : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → x++    If we clean up that type we get:++>     ∀(x : ./Nat )+> →   ∀(Nat : *)+> →   ∀(Succ : ∀(pred : Nat) → Nat)+> →   ∀(Zero : Nat)+> →   Nat++    Conceptually, when we fold a @./Nat@ value using @.\/Nat\/foldNat@ we just+    replace each @.\/Nat\/Succ@ constructor with the argument of the fold+    labeled @Succ@ (i.e. the third argument).  Similarly, we substitute each+    @.\/Nat\/Zero@ constructor with the fourth argument labeled @Zero@.++    We also supply a type parameter named @Nat@ as the second argument.  This+    type parameter must match the input and output of whatever we use to replace+    the @.\/Nat\/Succ@ and @.\/Nat\/Zero@.++    For example, suppose that we wanted to write a function to test if a @./Nat@+    was an even number.  We would just substitute every @Zero@ constructor with+    @.\/Bool\/True@ and substitute every @.\/Nat\/Succ@ constructor with+    @./not@.  The code for that would be:++> $ cat not.annah  # Update `not.annah` to use our new file layout+> let not (b : ./Bool ) : ./Bool =+>     ./Bool/if b ./Bool+>         ./Bool/False+>         ./Bool/True+> in  not++> $ cat isEven.annah +> let isEven (n : ./Nat ) : ./Bool =+>     ./Nat/foldNat n ./Bool+>         ./not       -- Replace every `./Nat/Succ` with `./not`+>         ./Bool/True -- Replace every `./Nat/Zero` with `./Bool/True`+> in  isEven++    The let definitions are not strictly necessary since we could just write:++> $ cat not.annah+> \(b : ./Bool ) ->+>     ./Bool/if b ./Bool+>         ./Bool/False+>         ./Bool/True++> $ cat isEven.annah+> \(n : ./Nat ) ->+>     ./Nat/foldNat n ./Bool+>         ./not+>         ./Bool/True++    ... but the let definitions help the readability of the code by naming the+    functions and documenting their expected return types.++    Then we can compile our Annah expression to Morte code:++> $ annah compile    not.annah > not+> $ annah compile isEven.annah > isEven++    ... and test that @./isEven@ works:++> $ morte+> ./isEven (./Nat/Succ (./Nat/Succ ./Nat/Zero ))+> <Ctrl-D>+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++    It works!  The result is identical to @.\/Bool\/True@:++> $ morte+> ./Bool/True+> <Ctrl-D>+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+>+> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True++    Conceptually, what happened was that @./isEven@ just performed the+    desired substitutions, replacing every @.\/Nat\/Succ@ with @./not@ and+    replacing every @.\/Nat\/Zero@ with @.\/Bool\/True@:++> ./isEven (./Nat/Succ (./Nat/Succ ./Nat/Zero ))+>+> -- Constructor substitution+> = ./not (./not ./Bool/True )+>+> -- β-reduce+> = ./Bool/True++    Note that this is not really the path the compiler takes under the hood, but+    it's equivalent.++    We can also encode mutually recursive types such as the following type+    declaration for even and odd numbers:++> $ annah+> type Even+> data SuccE (predE : Odd)+> data ZeroE+> fold foldEven+> +> type Odd+> data SuccO (predO : Even)+> fold foldOdd+> +> in SuccE (SuccO ZeroE)+> λ(Even : *) → λ(Odd : *) → λ(SuccE : ∀(predE : Odd) → Even) → λ(ZeroE : Even) → λ(SuccO : ∀(predO : Even) → Odd) → SuccE (SuccO ZeroE)++    Like before, we can encode each type and term separately as files and the+    files:++> annah types+> type Even+> data SuccE (predE : Odd)+> data ZeroE+> fold foldEven+> +> type Odd+> data SuccO (predO : Even)+> fold foldOdd+> <Ctrl-D>++    ... and now these files can be used to build @./Even@ or @./Odd@ values:++> $ morte+> ./Even/SuccE (./Odd/SuccO ./Even/ZeroE )+> <Ctrl-D>+> ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Even+> +> λ(Even : *) → λ(Odd : *) → λ(SuccE : ∀(predE : Odd) → Even) → λ(ZeroE : Even) → λ(SuccO : ∀(predO : Even) → Odd) → SuccE (SuccO ZeroE)++    We can also consume mutually recursive types just by folding them.  Each+    type is already a preformed fold and we can consult each type's respective+    @fold@ function to see what arguments the @fold@ expects:++> $ morte+> ./Even/foldEven+> <Ctrl-D>+> ∀(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Even) → ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Even+> +> λ(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Even) → x++> $ morte+> ./Odd/foldOdd+> ∀(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Odd) → ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Odd+> +> λ(x : ∀(Even : *) → ∀(Odd : *) → ∀(SuccE : ∀(predE : Odd) → Even) → ∀(ZeroE : Even) → ∀(SuccO : ∀(predO : Even) → Odd) → Odd) → x++    If we clean up the type of the @.\/Even\/foldEven@ function we get this:++>     ∀(x : ./Even )+> →   ∀(Even : *)+> →   ∀(Odd : *)+> →   ∀(SuccE : ∀(predE : Odd) → Even)+> →   ∀(ZeroE : Even)+> →   ∀(SuccO : ∀(predO : Even) → Odd)+> →   Even++    Conceptually, when we fold an @./Even@ value using @.\/Even\/foldEven@ we+    just replace each @.\/Even\/SuccE@ constructor with the argument of the fold+    labeled @SuccE@ (i.e. the fourth argument).  Similarly, we substitute each+    @.\/Even\/ZeroE@ constructor with the fifth argument named @ZeroE@ and+    substitute each @.\/Odd\/SuccO@ constructor with the sixth argument named+    @SuccO@.++    We also supply two type parameters named @Even@ and @Odd@.  These type+    parameters must match the input and output of whatever we use to replace+    the @SuccE@, @ZeroE@ and @SuccO@ constructors.++    For example, suppose that we wanted to write a function that converts an+    @./Even@ value to a @./Nat@.  We would just replace every @.\/Even\/SuccE@+    and @.\/Odd\/SuccO@ constructor with @Succ@ and replace every+    @.\/Even\/ZeroE@ constructor with @Zero@, like this:++> $ cat evenToNat.annah+> let evenToNat (e : ./Even ) : ./Nat =+>     ./Even/foldEven e ./Nat ./Nat+>         ./Nat/Succ  -- Replace every `./Even/SuccE` with `Succ`+>         ./Nat/Zero  -- Replace every `./Even/ZeroE` with `Zero`+>         ./Nat/Succ  -- Replace every `./Odd/SuccO`  with `Succ`+> in  evenToNat++    Now we can \"compile\" our @evenToNat@ function to Morte code:++> annah evenToNat.annah > evenToNat++    ... and test that it correctly converts @./Even@ values to their+    equivalent @./Nat@ values:++> $ morte+> ./evenToNat (./Even/SuccE (./Odd/SuccO ./Even/ZeroE ))+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ Zero)++    It works!  We can began with the number two, encoded as an @./Even@ number+    and ended with two encoded as a @./Nat@.++    As before, the @./evenTonat@ function was just performing the desired+    substitution, replacing each @.\/Even\/SuccE@ and @.\/Odd\/SuccO@ with+    @.\/Nat\/Succ@ and replacing @.\/Odd\/ZeroE@ with @.\/Nat\/Zero@:++> ./evenToNat (./Even/SuccE (./Odd/SuccO ./Even/ZeroE ))+>+> -- Constructor substitution+> = ./Nat/Succ (./Nat/Succ ./Nat/Zero )++    Again, this is not the path the compiler takes under the hood, but it's+    equivalent.+-}++{- $prelude+    Annah also comes with a Prelude of utility types and terms.  This Prelude is+    hosted remotely here:++    <http://sigil.place/prelude/annah/1.0/>++    You can visit the above link to browse the Prelude and see what is+    available.++    There are several ways that you can use the Prelude.  The most direct+    approach is to use expressions from the Prelude directly by referencing+    their URLs, like this:++> $ morte+> http://sigil.place/prelude/annah/1.0/Nat/Succ+> (   http://sigil.place/prelude/annah/1.0/Nat/Succ+>     (   http://sigil.place/prelude/annah/1.0/Nat/Succ+>         http://sigil.place/prelude/annah/1.0/Nat/Zero+>     )+> )+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))++    ... or you can selectively \"alias\" remote references locally by creating+    local files that refer to the remote URLs:++> $ echo "http://sigil.place/prelude/annah/1.0/Nat/Succ" > Succ+> $ echo "http://sigil.place/prelude/annah/1.0/Nat/Zero" > Zero+> $ morte+> ./Succ (./Succ (./Succ ./Zero ))+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero))++    ... or you can \"import\" the entire Prelude into your current directory+    using @wget@:++> $ wget -np -r --cut-dirs=3 http://sigil.place/prelude/annah/1.0/+> $ cd sigil.place+> $ ls+> (->)            Defer.annah    List.annah    Path         Sum0.annah+> (->).annah      Eq             Maybe         Path.annah   Sum1+> Bool            Eq.annah       Maybe.annah   Prod0        Sum1.annah+> Bool.annah      Functor        Monad         Prod0.annah  Sum2+> Category        Functor.annah  Monad.annah   Prod1        Sum2.annah+> Category.annah  index.html     Monoid        Prod1.annah+> Cmd             IO             Monoid.annah  Prod2+> Cmd.annah       IO.annah       Nat           Prod2.annah+> Defer           List           Nat.annah     Sum0++    This tutorial will assume that you have imported the Prelude locally.++    The Prelude is organized according to the following rules:++    * Each type (like @./Bool@ or @./Nat@) is a top-level directory.  You can+      reference that type in your code by its directory+    * Each constructor of that type lives underneath the type's directory.  For+      example, @True@ is located underneath the @./Bool@ directory+    * Functions associated with each type are also located underneath the type's+      directory.  For example, the @length@ function is located underneath the+      @./List@ directory.+    * Every expression is provided as both the original Annah code (with a+      @*.annah@ suffix) and Morte code (with no suffix).  For example, you+      will find the @Monoid.annah@ file which was the Annah expression used to+      create the @Monoid@ file which is a Morte expression.++    In order to use an expression within Morte you must explicitly import the+    expression within the Morte code, like this:++> $ echo "./List/length" | morte  # Good+> ∀(a : *) → ∀(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Nil : Nat) → Nat+> +> λ(a : *) → λ(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → xs Nat (λ(_ : a) → Succ)++    Reading the expression through standard input will (usually) not work:++> $ morte < List/length  # Bad+> ../List: openFile: does not exist (No such file or directory)++    The reason why is that everything in the Prelude uses relative imports to+    reference each other.  This is what allows the Prelude to correctly+    function both when you reference the Prelude remotely and when you download+    the Prelude locally.  If you read the expression through standard input+    then Morte incorrectly concludes that any further imports are relative to+    your current directory.  However, if you explicitly import the expression+    within the code then Morte correctly concludes that transitive imports are+    relative to the imported file's path.++    For example, the @List/length@ file has the following contents:++> cat List/length+> λ(a : *) → λ(xs : ../List  a) → λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → xs Nat (λ(_ : a) → Succ)++    There is one relative reference within that file to @../List@.  That+    reference is relative to the current file's directory (i.e. relative to+    @List/@) which means that it still points to the same directory: @List@.  We+    could have also used just @.@ to refer to the current directory but that+    would be less readable.++    However, if you read in @List/length@ from standard input, then @morte@+    looks for @../List@ expression relative to your present working directory+    and fails.++    Annah's Prelude has some similarities to Haskell's standard libraries and+    some differences.  The rough correspondences are:++    * @(->)@ corresponds to Haskell's @(->)@ type constructor+    * @Bool@ corresponds to Haskell's `Bool` type+    * @Cmd@ corresponds to the operational monad (i.e.+      "Control.Monad.Operational".`Control.Monad.Operational.Program`)+    * @Defer@ corresponds to+      "Data.Functor.Coyoneda".`Data.Functor.Coyoneda.Coyoneda`+    * @List@ corresponds to Haskell lists except that Annah @List@s are always+      finite because they are encoded recursively+    * @Maybe@ corresponds to Haskell's `Maybe` type constructor+    * @Nat@ corresponds to Haskell's `Numeric.Natural.Natural` type, except+      much less efficient than its Haskell counterpart+    * @Path@ corresponds to a free category.  As far as I know there is no+      standard Haskell implementation for free categories to reference+    * @Prod0@ corresponds to Haskell's @()@ type.  Mnemonic: \"Product type with+      zero fields\"+    * @Prod1@ corresponds to Haskell's `Data.Functor.Identity` type constructor.+      Mnemonic: \"Product type with one field\"+    * @Prod2@ corresponds to Haskell's 2-tuple type constructor.  Mnemonic:+      \"Product type with two fields\"+    * @Sum0@ corresponds to Haskell's `Data.Void.Void` type.  Mnemonic: \"Sum+      type with zero fields\"+    * @Sum1@ also corresponds to Haskell's `Data.Functor.Identity` type+      constructor.  Mnemonic: \"Sum type with one field\"+    * @Sum2@ corresponds to Haskell's `Either` type constructor.  Mnemonic:+      \"Sum type with two fields\"+    * @IO@ corresponds to a very simple `IO` type constructor that only supports+      two operations:++      > ./IO/get : ./IO ./Nat+      > ./IO/put : ./Nat -> ./IO ./Prod0++    In addition to those types, Annah also encodes several of Haskell's type+    classes as values.  Neither Annah nor Morte supports type classes /per se/.+    Instead, each class is encoded as a type constructor and each instance is+    a term of the corresponding type:++    * @Functor@ corresponds to Haskell's `Functor` class+    * @Monoid@ corresponds to Haskell's `Data.Monoid.Monoid` class+    * @Monad@ corresponds to Haskell's `Monad` class+    * @Category@ corresponds to Haskell's `Control.Category.Category` class++    However, the specification of each type class radically differs from how+    Haskell encodes things.  We'll revisit this in a later section.+-}++{- $nats+    The Prelude provides addition and multiplication for natural numbers:++> $ cat > three+> ./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))+> <Ctrl-D>++> $ morte+> ./Nat/(+) ./three ./three+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero)))))++> $ morte+> ./Nat/(*) ./three ./three+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))++    Also, Annah provides basic syntactic support for natural number literals:++> $ annah | morte+> ./Nat/(+) 3 3+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero)))))++> $ annah | morte+> ./Nat/(*) 3 3+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))++-}++{- $lists+    The Prelude provides operations on lists, too:++> $ annah | morte+> ./List/replicate ./Bool 3 ./Bool/True+> <Ctrl-D>+> ∀(List : *) → ∀(Cons : ∀(head : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(tail : List) → List) → ∀(Nil : List) → List+> +> λ(List : *) → λ(Cons : ∀(head : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → ∀(tail : List) → List) → λ(Nil : List) → Cons (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) (Cons (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) (Cons (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True) Nil))++    Annah also provides support for list literals:++> $ annah > bools+> [nil ./Bool , ./Bool/True , ./Bool/False , ./Bool/True ]+> <Ctrl-D>++> $ cat bools+> λ(List : *) → λ(Cons : ∀(head : ./Bool ) → ∀(tail : List) → List) → λ(Nil : List) → Cons ./Bool/True  (Cons ./Bool/False  (Cons ./Bool/True  Nil))++    The general format for lists is:++> [nil elementType, element0, element1, ..., elementN]++    Here are some examples of operations on lists:++> $ morte+> ./List/null ./Bool ./bools+> <Ctrl-D>+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False++> $ morte+> ./List/length ./Bool (./List/(++) ./Bool ./bools ./bools )+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Nil : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Nil : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Nil)))))++> $ annah | morte+> \(a : *) -> \(xs : ./List a) -> ./List/(++) a xs [nil a]+> <Ctrl-D>+> ∀(a : *) → ∀(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → ∀(List : *) → ∀(Cons : a → List → List) → ∀(Nil : List) → List+> +> λ(a : *) → λ(xs : ∀(List : *) → ∀(Cons : ∀(head : a) → ∀(tail : List) → List) → ∀(Nil : List) → List) → xs++    The last example shows how @morte@ can optimized away @xs ++ []@ to just+    @xs@.+-}++{- $monoids+    Annah also provides several folds on lists, like @sum@ or @and@:++> $ annah | morte+> <Ctrl-D>+> ./Nat/sum [nil ./Nat , 1, 2, 3, 4]+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))++> $ annah | morte+> <Ctrl-D>+> ./Bool/and [nil ./Bool , ./Bool/True , ./Bool/False , ./Bool/True ]+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False++    What's interesting about these folds is their type:++> $ cat Nat/sum.annah+> let sum : ../Monoid ../Nat = \(xs : ../List ../Nat ) -> xs ../Nat ./(+) 0+> in  sum++> $ cat Bool/and.annah+> let and : ../Monoid ../Bool =+>     \(xs : ../List ../Bool ) -> xs ../Bool ./(&&) ./True+> in  and++    You might have been expecting their types to be something like this:++> sum : ../List ../Nat  -> ../Nat+> and : ../List ../Bool -> ../Bool++    ... and you would have been right because that is actually what their types+    are!  This is because of how @./Monoid.annah@ is defined:++> $ cat Monoid.annah+> let Monoid (m : *) : * = ./List m -> m+> in  Monoid++    In other words, a `Monoid` \"instance\" for a type @m@ is just a function+    that folds a @./List@ of @m@s into a single @m@.  The @./sum@ and @./and@+    functions that fold lists also double as @./Monoid@ instances.++    You can recover the traditional Haskell `Monoid` operations like `mempty`+    and `mappend` from the above @./Monoid@ definition:++> $ cat Monoid/mempty.annah+> let mempty (m : *) (monoid : ./Monoid m) : m =+>     monoid [nil m]+> in  mempty++> $ cat Monoid/mappend.annah+> let mappend (m : *) (monoid : ./Monoid m) (l : m) (r : m) : m =  +>     monoid [nil m, l, r]+> in  mappend++    For example:++> $ morte+> ./Monoid/mempty ./Nat ./Nat/sum+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Zero++> $ annah | morte+> ./Monoid/mappend ./Nat ./Nat/sum 4 5+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))++    However, in practice it's easier to just use the folds directly instead of+    using @.\/Monoid\/mempty@ or @.\/Monoid\/mappend@:++> $ annah | morte+> ./Nat/sum [nil ./Nat ]+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Zero++> $ annah | morte+> ./Nat/sum [nil ./Nat , 4, 5]+> <Ctrl-D>+> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat+> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))+-}++{- $commands+    Annah also provides syntactic support for chaining commands using @do@+    notation, in a style very similar to Haskell.  The following examples will+    all give very large outputs so I will tidy the output results, although+    there is not a good way to tidy the output in general:++    For example, here is how you write a list comprehension in Annah.++> $ annah | morte  # Output cleaned up by hand+> ./List/Monad ./Nat (do ./List {+>     x : ./Nat <- [nil ./Nat , 1, 2, 3];+>     y : ./Nat <- [nil ./Nat , 4, 5, 6];+>     _ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);+> })+> <Ctrl-D>+>     ∀(List : *)+> →   ∀(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List) → List)+> →   ∀(Nil : List)+> →   List+> +>     λ(List : *)+> →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List) → List)+> →   λ(Nil : List)+> →   Cons+>     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ Zero)))))+>     (   Cons+>         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero))))))+>         (   Cons+>             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))+>             (   Cons+>                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero))))))+>                 (   Cons+>                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))+>                     (   Cons+>                         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))+>                         (   Cons+>                             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))+>                             (   Cons+>                                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))+>                                 (   Cons+>                                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))+>                                     Nil+>                                 )+>                             )+>                         )+>                     )+>                 )+>             )+>         )+>     )++    ... which is equivalent to:++> ./List ./Nat+>+> [nil ./Nat , 5, 6, 7, 6, 7, 8, 7, 8, 9]++    Annah @do@ notation has a few important differences from Haskell's @do@+    notation:++    * Every command's return type must be annotated; even the final command+    * Braces are required and semicolons are required on all lines+    * You must annotate the monad's type constructor right after the @do@+    * You (usually) wrap the @do@ block in the @./Monad@ instance for your+      type constructor followed by the @do@ block's return value++    Here is an example diagram to illustrate the last rule:++> +-- Monad instance for ./List+> |+> |            +-- The return value of block ...+> |            |+> v            v+> ./List/Monad ./Nat (do ./List {+>     x : ./Nat <- [nil ./Nat , 1, 2, 3];+>     y : ./Nat <- [nil ./Nat , 4, 5, 6];+>     _ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);+> })      ^+>         |+>         +-- ... which must match this return value++    You actually don't have to wrap the @do@ block in a @./Monad@ instance, but+    you will get a different result.  Let's see what happens if we omit the+    @./Monad@ instance:++> $ annah | morte  # Output cleaned up by hand+> do ./List {+>     x : ./Nat <- [nil ./Nat , 1, 2, 3];+>     y : ./Nat <- [nil ./Nat , 4, 5, 6];+>     _ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);+> }+> <Ctrl-D>+>     ∀(Cmd : *)+> →   ∀(Bind : ∀(b : *) → (∀(List : *) → ∀(Cons : ∀(head : b) → ∀(tail : List) → List) → ∀(Nil : List) → List) → (b → Cmd) → Cmd)+> →   ∀(Pure : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Cmd)+> →   Cmd+>+>     λ(Cmd : *)+> →   λ(Bind : ∀(b : *) → (∀(List : *) → ∀(Cons : ∀(head : b) → ∀(tail : List) → List) → ∀(Nil : List) → List) → (b → Cmd) → Cmd)+> →   λ(Pure : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Cmd)+> →   Bind+>     (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat)+>     (   λ(List : *)+>     →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List) → List)+>     →   λ(Nil : List)+>     →   Cons+>         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → Succ)+>         (   Cons+>             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ Zero))+>             (   Cons+>                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ Zero)))+>                 Nil+>             )+>         )+>     )+>     (   λ(x : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat)+>     →   Bind+>         (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat)+>         (   λ(List : *)+>         →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List) → List)+>         →   λ(Nil : List)+>         →   Cons+>             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>             (   Cons+>                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ Zero)))))+>                 (   Cons+>                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ (Succ (Succ Zero))))))+>                     Nil+>                 )+>             )+>         )+>         (   λ(y : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat)+>         →   Bind+>             (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat)+>             (   λ(List : *)+>             →   λ(Cons : ∀(head : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → ∀(tail : List) → List)+>             →   Cons+>                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → x Nat Succ (y Nat Succ Zero))+>             )+>             Pure+>         )+>     )++    ... which is equivalent to:++> ./Cmd ./List./Nat+>+>     λ(Cmd : *)+> →   λ(Bind : ∀(b : *) → ./List b → (b → Cmd) → Cmd)+> →   λ(Pure : ./Nat → Cmd)+> →   Bind+>     ./Nat+>     [nil ./Nat , 1, 2, 3]+>     (   λ(x : ./Nat )+>     →   Bind+>         ./Nat+>         [nil ./Nat 4, 5, 6]+>         (   λ(y : ./Nat )+>         →   Bind+>             ./Nat+>             [nil ./Nat (./Nat/(+) x y)]+>             Pure+>         )+>     )++    The @do@ notation is desugaring to a data type named @./Cmd@ that inserts+    placeholders for each @<-@ (pronounced: \"bind\").  In the Haskell world+    this datatype is commonly known as the \"operational\" monad.++    So why did we wrap the @do@ block in @.\/List\/Monad@?  Well, let's check+    out the type of the @.\/List\/Monad@ function:++> $ cat ./List/Monad.annah +> let Monad: ../Monad ../List+>     =   \(a : *)+>     ->  \(m : ../Cmd ../List a)+>     ->  m (../List a) (\(b : *) -> ./(>>=) b a) (./pure a)+> in  Monad++    Hmmm, that's weird.  Wasn't it supposed to be a function?  Actually, it is!+    To see why, let's check out how @./Monad@ is defined:++> let Monad (m : * -> *) : * = forall (a : *) -> ./Cmd m a -> m a+> in  Monad++    A @./Monad m@ is a function that transforms a @./Cmd m a@ into an @m a@ by+    replacing each @Bind@ with the correct \"bind\" operation for that `Monad`+    and replaces each @Pure@ with the correct \"pure\" operation for that+    `Monad`.  Therefore a @./Monad ./List@ is a function that transforms a+    @.\/Cmd .\/List a@ into a @./List a@.++    That's why we wrap the @do@ block in @.\/List\/Monad@ because the @do@+    block starts out with this type:++> do ./List { ... } : ./Cmd ./List ./Nat++    ... and then when we apply the @.\/List\/Monad function we get back a+    bona-fide @./List@:++> ./List/Monad ./Nat (do ./List { ... }) ./List ./Nat++    There are a couple of parallels between Annah's @./Monad@+@./Cmd@ and+    Annah's @./Monoid@+@./List@:++    * Both of them have syntactic support for building a placeholder of some+      sort.  List notation builds a @./List@ and @do@ notation builds a @./Cmd@+    * Both of them have a way to fold the placeholder into a single value.+      @./Monoid@s fold @./List@s and @./Monad@s fold @./Cmd@s.++-}++{- $io++    Annah also supports a very simplistic @./IO@ type as a proof of concept for+    how you would model a foreign function interface.  For example, here is an+    @./IO@ action that reads a @./Nat@ and writes out the same @./Nat@:++> $ annah+> ./IO/Monad ./Prod0 (do ./IO {+>     n : ./Nat   <- ./IO/get  ;+>     _ : ./Prod0 <- ./IO/put n;+> })+> <Ctrl-D>+> ./IO/Monad  ./Prod0  (λ(Cmd : *) → λ(Bind : ∀(b : *) → ./IO  b → (b → Cmd) → Cmd) → λ(Pure : ./Prod0  → Cmd) → Bind ./Nat  ./IO/get  (λ(n : ./Nat ) → Bind ./Prod0  (./IO/put  n) Pure))++    Annah also provides utilities similar to Haskell for chaining commands, such+    as @.\/Monad\/replicateM_.annah@ which lets you repeat a command a fixed+    number of times:++> $ cat Monad/replicateM_.annah+> let replicateM_ (m : * -> *) (n : ../Nat ) (cmd : m ../Prod0 )+>   : ../Cmd m ../Prod0+>   = ./sequence_ m (../List/replicate (m ../Prod0 ) n cmd)+> in  replicateM_++    Notice that @.\/Monad\/replicateM_@ does not take a @./Monad@ instance as+    an argument.  Instead, @.\/Monad\/replicateM_@ returns a @./Cmd@ which+    you can fold with the appropriate @./Monad@ instance:++    For example:++> $ annah | morte  # Output cleaned up by hand+> ./IO/Monad ./Prod0 (./Monad/replicateM_ ./IO 10 (./IO/put 4))+>     ∀(IO : *)+> →   ∀(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) → IO)+> →   ∀(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO → IO)+> →   ∀(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO)+> →   IO+> +>     λ(IO : *)+> →   λ(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) → IO)+> →   λ(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO → IO)+> →   λ(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO)+> →   Put_+>     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>     (   Put_+>         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>         (   Put_+>             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>             (   Put_+>                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                 (   Put_+>                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                     (   Put_+>                         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                         (   Put_+>                             (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                             (   Put_+>                                 (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                                 (   Put_+>                                     (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                                     (   Put_+>                                         (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ (Succ (Succ Zero))))+>                                         (Pure_ (λ(Prod0 : *) → λ(Make : Prod0) → Make))+>                                     )+>                                 )+>                             )+>                         )+>                     )+>                 )+>             )+>         )+>     )++    If you clean that up a bit you get a syntax tree for printing @4@ 10 times:++>     λ(IO : *)+> →   λ(Get_ : (./Nat → IO) → IO)+> →   λ(Put_ : ./Nat → IO → IO)+> →   λ(Pure_ : ./Prod0 → IO)+> →   Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Put_ 4 (Pure_ ./Prod0/Make ))))))))))++    Let's try a more complicated program, that reads and writes integers 10+    times:++> $ annah | morte+> let io : ./IO ./Prod0 = ./IO/Monad ./Prod0 (do ./IO {+>     n : ./Nat   <- ./IO/get  ;+>     _ : ./Prod0 <- ./IO/put n;+> })+> in  ./IO/Monad ./Prod0 (./Monad/replicateM_ ./IO 10 io)+> <Ctrl-D>+> ∀(IO : *) → ∀(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) → IO) → ∀(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO → IO) → ∀(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO) → IO+> +> λ(IO : *) → λ(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO) → IO) → λ(Put_ : (∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO → IO) → λ(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO) → Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ r (Pure_ (λ(Prod0 : *) → λ(Make : Prod0) → Make)))))))))))))))))))))++    ... which if we simplify we get:++>     λ(IO : *)+> →   λ(Get_ : (./Nat → IO) → IO)+> →   λ(Put_ : ./Nat → IO → IO)+> →   λ(Pure_ : ./Prod0 → IO)+> →   Get_ (λ(r : ./Nat ) →+>       Put_ r (+>         Get_ (λ(r : ./Nat ) →+>           Put_ r (+>             Get_ (λ(r : ./Nat ) →+>               Put_ r (+>                 Get_ (λ(r : ./Nat ) →+>                   Put_ r (+>                     Get_ (λ(r : ./Nat ) →+>                       Put_ r (+>                         Get_ (λ(r : ./Nat ) →+>                           Put_ r (+>                             Get_ (λ(r : ./Nat ) →+>                               Put_ r (+>                                 Get_ (λ(r : ./Nat ) →+>                                   Put_ r (+>                                     Get_ (λ(r : ./Nat ) →+>                                       Put_ r (+>                                         Get_ (λ(r : ./Nat ) →+>                                           Put_ r (+>                                             Pure_ ./Prod0/Make))))))))))))))))))))++    In other words, we've built an abstract syntax tree representing ten+    @Get_@ and @Put_@ nodes where each @Get_@ node threads its result to the+    next @Put_@ node.++    Annah cannot run this abstract syntax tree since Annah does not have a+    backend to interpret this tree.  The most Annah can do is model effects+    without running them.+-}++{- $paths+    Annah provides support for the `Category` type class, too, using an approach+    very similar to the support for `Monoid` and `Monad`:++    * Provide a placeholder type named @./Path@ (which is a \"free category\")+    * Provide syntactic support for building @./Path@s+    * Define a @./Category@ to be something that folds @./Path@s++> $ cat Category.annah+> let Category (cat : * -> * -> *) : * =+>     forall (a : *) -> forall (b : *) -> ./Path cat a b -> cat a b+> in  Category++    Here is an example of composing several functions using the @./Category@+    instance for functions:++> $ annah | morte+> let even (n : ./Nat ) : ./Bool = n ./Bool ./Bool/not ./Bool/True+>+> in  let f : ./List ./Nat -> ./Bool =+>     ./(->)/Category (./List ./Nat ) ./Bool+>         [id ./(->) { ./List ./Nat } ./Nat/sum { ./Nat } even { ./Bool } ./Bool/not { ./Bool }]+>+>     in  f [nil ./Nat , 1, 2, 3, 4+> <Ctrl-D>+> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool+> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False++    The above code creates a composition chain of three functions, reading from+    left to right:++    * @.\/Nat/sum@, which has type @.\/List .\/Nat -> .\/Nat@+    * @even@, which has type @.\/Nat -> .\/Bool@+    * @.\/Bool\/not@, which has type @.\/Bool -> .\/Bool@++    Annah's path notation requires you to annotate the types along the way as+    you compose each component.  In the above example, you can find each+    function's input type immediately to the left of that function and the+    output type immediately to the right of each function.  Types are surrounded+    by braces to separate them from the things you compose.++    Annah's path notation differs from lists in a couple of ways:++    * You replace @nil@ with @id@+    * The @id@ is followed by the type constructor that you are chaining+    * You replace commas with intermediate types++    You may find the notation easier to read if you put each composable+    component on a separate line preceded by the corresponding input type:++> let even (n : ./Nat ) : ./Bool = n ./Bool ./Bool/not ./Bool/True+>+> in  let f : ./List ./Nat -> ./Bool =+>     ./(->)/Category (./List ./Nat ) ./Bool [id ./(->)+>         { ./List ./Nat } ./Nat/sum+>         { ./Nat        } even+>         { ./Bool       } ./Bool/not+>         { ./Bool       }+>     ]+>+>     in  f [nil ./Nat , 1, 2, 3, 4]++    Annah's Prelude only provides support for one @./Category@ instance for+    functions named @./(->)/Category@, so in practice the @./Category@ support+    is not that handy out-of-the box and is mainly provided for completeness.+-}++{- $conclusion+    Those are all the features that Annah supports!  Annah is a very tiny+    language and library that illustrates and implements basic idioms for+    translating functional programming concepts into pure lambda calculus.++    Hopefully you can use Annah to learn how to encode a subset of Haskell in a+    completely total programming language.  If you translate any Haskell+    functions to Annah you can contribute them upstream to the Annah prelude by+    submitting a pull request against the Annah repository:++    <https://github.com/Gabriel439/Haskell-Annah-Library/tree/master/Prelude>+-}