---
slug: "locque"
source_type: "readme"
source_url: "https://cdn.jsdelivr.net/gh/jaggederest/locque@main/README.md"
repo: "https://github.com/jaggederest/locque"
source_file: "README.md"
branch: "main"
---
# Locque

Locque is a dependently typed language designed to be easy for both humans and LLMs to read, write, and refactor. It uses explicit keywords, a strict value/computation split, and a 1:1 mapping between M-expressions (human-friendly) and S-expressions (AST-exact).

Note: Locque is built almost entirely by LLMs; no human coding has been used.

## For a broad audience

If you want a language that is:
- explicit and predictable (no hidden coercions),
- precise about effects (computations are marked and performed explicitly),
- friendly to tools and automation,
then Locque is aimed at you.

Here is a small example:

```locque
import io as IO
import string as S

module examples::hello contains
  define transparent main as compute
    perform (IO::print (S::concat "hello, " "world"))
  end
end
```

You can also define your own data types and pattern match explicitly:

```locque
module examples::maybe contains
  define transparent Option as data A Type0 in Type0
    case Option::none of-type Option A
    case Option::some of-type for-all x as A to Option A
  end

  define transparent get-or as
    function A Type0 fallback A opt (Option A) returns A value
      match opt of-type (Option A) as ignored returns A
        case Option::none as fallback
        case Option::some with x A as x
      end
    end
end
```

## For vibe coders

Locque is intentionally verbose. The structure is always visible, so refactors are safe and repeatable. You do not need to guess operator precedence or implicit conversions. The language is built to help LLMs stay consistent and to help humans audit what was generated.

If you enjoy quick iterations, the workflow is simple:
- edit `.lq` files,
- run `smyth test`,
- repeat.

## For mathematicians

Locque is dependent and explicit:
- universes are strict (`Type0`, `Type1`, ...),
- Pi and Sigma are core (`for-all`, `there-exists`),
- equality is first-class (`equal`, `reflexive`, `rewrite`),
- definitional equality is intentionally small (beta/delta/iota).

Values are total and normalize; computations are explicitly marked and only run via `perform`. This makes the value world suitable for proofs and types, while still supporting effectful programs in the computation world.

## Formatting

Locque uses a strict, simple indentation style:
- 2 spaces per block level; tabs are not allowed.
- `end` aligns with the block it closes.
- `case ... as` with a multiline body puts the body on the next line, indented one level.
- Multi-line applications may indent continuation lines one extra level.

Check formatting with `smyth format [path]` (a file or directory; defaults to `lib/`, `test/`, and `Smythfile.lq` under the Smythfile.lq directory). `--edit`/`--in-place` are reserved but not implemented yet.

## Contributing

- License: MIT. See `LICENSE`.
- Repo: https://github.com/jaggederest/locque/
- PRs: fork, create a branch, make focused changes, and open a PR.
- Tooling: install GHC to build `locque-interpreter` and `smyth` (https://www.haskell.org/ghcup/).
- Tests: run `smyth test` from the repo root to check the full suite and expected failures (prints total time in microseconds). Use `smyth test --slow` to list the slowest suites.
- Benchmarks: run `smyth bench` from the repo root to see benchmark timings and threshold checks.

Reference grammar and canonical syntax live in `grammar.md`.

Copyright 2025-2026 Justin George.