diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/annah.cabal b/annah.cabal new file mode 100644 --- /dev/null +++ b/annah.cabal @@ -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 diff --git a/exec/Main.hs b/exec/Main.hs new file mode 100644 --- /dev/null +++ b/exec/Main.hs @@ -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 ) ) diff --git a/src/Annah/Core.hs b/src/Annah/Core.hs new file mode 100644 --- /dev/null +++ b/src/Annah/Core.hs @@ -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) diff --git a/src/Annah/Lexer.x b/src/Annah/Lexer.x new file mode 100644 --- /dev/null +++ b/src/Annah/Lexer.x @@ -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) +} diff --git a/src/Annah/Parser.hs b/src/Annah/Parser.hs new file mode 100644 --- /dev/null +++ b/src/Annah/Parser.hs @@ -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) diff --git a/src/Annah/Tutorial.hs b/src/Annah/Tutorial.hs new file mode 100644 --- /dev/null +++ b/src/Annah/Tutorial.hs @@ -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: + + + + 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: + + + + 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 +> +> λ(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 +> +> λ(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 +> +> λ(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 +> +> λ(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)) +> +> λ(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 +> +> ∀(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 +> +> ∀(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 +> + + ... 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 +> +> * +> +> ∀(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 +> +> ∀(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 +> +> 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 +> + + 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)) +> +> λ(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 +> + + ... and now we can build natural numbers using these files: + +> $ morte +> ./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero )) +> +> ∀(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 )) +> +> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool +> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True + + It works! The result is identical to @.\/Bool\/True@: + +> $ morte +> ./Bool/True +> +> ∀(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 +> + + ... and now these files can be used to build @./Even@ or @./Odd@ values: + +> $ morte +> ./Even/SuccE (./Odd/SuccO ./Even/ZeroE ) +> +> ∀(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 +> +> ∀(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: + + + + 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 +> ) +> ) +> +> ∀(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 )) +> + +> $ 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 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 +> +> ∀(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 +> +> ∀(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 ] +> + +> $ 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 +> +> ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool +> +> λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False + +> $ morte +> ./List/length ./Bool (./List/(++) ./Bool ./bools ./bools ) +> +> ∀(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] +> +> ∀(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 +> +> ./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 +> +> ./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 +> +> ∀(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 +> +> ∀(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 ] +> +> ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat +> +> λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Zero + +> $ annah | morte +> ./Nat/sum [nil ./Nat , 4, 5] +> +> ∀(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); +> }) +> +> ∀(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); +> } +> +> ∀(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; +> }) +> +> ./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) +> +> ∀(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 +> +> ∀(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: + + +-}