morte-1.2.0: A bare-bones calculus of constructions

Safe HaskellNone




Morte lets you import external expressions located either in local files or hosted on network endpoints.

To import a local file as an expression, just prepend the file path with a hash tag. For example, suppose we had the following three local files:

-- id
\(a : *) -> \(x : a) -> x
-- Bool
forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True
-- True
\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True

You could then reference them within a Morte expression using this syntax:

#id #Bool #True

... which would embed their expressions directly within the syntax tree:

-- ... expands out to:
(\(a : *) -> \(x : a) -> x)
    (forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> True)
    (\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True)

Imported expressions may contain imports of their own, too, which will continue to be resolved. However, Morte will prevent cyclic imports. For example, if you had these two files:

-- foo
-- bar

... Morte would throw the following exception if you tried to import foo:

⤷ #foo
⤷ #bar
Cyclic import: #foo

You can also import expressions hosted on network endpoints. Just use a hashtag followed by a URL:


The compiler expects the downloaded expressions to be in the same format as local files, specifically UTF8-encoded source code text.

For example, if our id expression were hosted at, then we would embed the expression within our code using:


You can also reuse directory names as expressions. If you provide a path to a local or remote directory then the compiler will look for a file named @ within that directory and use that file to represent the directory.



load :: Expr Path -> IO (Expr X) Source

Resolve all imports within an expression

newtype Cycle Source

An import failed because of a cycle import




cyclicImport :: Path

The offending cyclic import

newtype ReferentiallyOpaque Source

Morte tries to ensure that all expressions hosted on network endpoints are weakly referentially transparent, meaning roughly that any two clients will compile the exact same result given the same URL.

To be precise, a strong interpretaton of referential transparency means that if you compiled a URL you could replace the expression hosted at that URL with the compiled result. Let's term this "static linking". Morte (very intentionally) does not satisfy this stronger interpretation of referential transparency since "statically linking" an expression (i.e. permanently resolving all imports) means that the expression will no longer update if its dependencies change.

In general, either interpretation of referential transparency is not enforceable in a networked context since one can easily violate referential transparency with a custom DNS, but Morte can still try to guard against common unintentional violations. To do this, Morte enforces that a non-local import may not reference a local import.

Local imports are defined as:

  • A file
    • A URL with a host of localhost or

    All other imports are defined to be non-local




opaqueImport :: Path

The offending opaque import

data Imported e Source

Extend another exception with the current import stack




importStack :: [Path]

Imports resolved so far, in reverse order

nested :: e

The nested exception