Corbenic is a glyph-based lazy, call-by-need, purely functional programming language.

note: Corbenic is very early in development and this site and page will be pretty at some point, but for now, it’s just going to serve as a single-page spec. This specification assumes familiarity with Haskell, as much of the language’s design is derived from Haskell.

The repository for Corbenic is on GitHub.

The recommended font for Corbenic code is Fairfax HD, which can be acquired here.

Philosophy of Corbenic

Glyphs Should Do One Specific Thing As Generally As Possible

This sounds oxymoronic, but hear me out.

In Haskell, there’s a composition operator (.). It has type (b → c) → (a → b) → a → c. You use it to apply one function to the result of another.

Corbenic also has a composition operator, it’s called «∘». However, if you investigate the type of «∘», what you will find is not the same:

«∘» ⠛ ∀c t₁ t₂ t₃. Semigroupoid c ⇒ c t₂ t₃ → c t₁ t₂ → c t₁ t₃

This is much more abstract, but if you dig into the category theory, it is indeed simply a generalization of Haskell’s operator! Semigroupoid is the class of types that support an associative composition in this way, so why not? Why shouldn’t the “fundamental” glyph do both?

However, there are times when glyphs do need to be genuinely different, because they’re doing genuinely different things. Haskell uses the type keyword for both type aliases and constraint aliases. Yes, constraints are types, but saying “something being considered a group means it is associative unital monoid” is not the same as saying “a Foo is a Bar”. So Corbenic uses two different glyphs to declare each.

Unicode is a Vast Banquet and We Would Be Fools to Not Partake Of It

Things in the Prelude will generally get their own glyphs (if there’s some glyph which can be at least somewhat non-arbitrarily be assigned to it and it isn’t a typeclass, since those are best left spelled).

Unicode has over a hundred thousand characters, so we will never run out (even if we limit ourselves to symbols, at first). We have reserved some characters as suffixes so related-but-not-the-same things can be named similarly, so we will be able to keep the language terse yet still very expressive, which leads us to….

Keep Your Head In The Clouds And Your Feet On The Ground

In some circles, functional programming langauges have an undeserved reputation for being overly academic ivory towers that aren’t used to do anything productive (if you don’t believe me that this reputation is undeserved, look into how many places use Haskell or OCaml when correctness starts to really matter…). If you were to ask Corbenic whether it thinks the abstractions seen in advanced functional programming are a bit too much, Corbenic (or perhaps more accurately the Roi Méhaigné) would reply “Of course not! I love abstract nonsense!”

As such, the Prelude is chock full of such abstractions in the hope that someone might find them useful one day, even if only to golf down a few characters. The language itself will also slowly gain more type level wizardry over time (as fast as the writer can implement it…)

That being said, abstractions are only useful if you have things to use them on, so the Prelude will also try to be full of generally useful machinery that many languages delegate to external dependencies. Furthermore, the link between the cloud and the ground should be maximally strong: If you find that something in the Prelude should have a Profunctor or Comonad or CommutativeRing instance and it doesn’t, that’s a bug, and you should tell me about it!

Identifiers

In Corbenic, most predefined functions and operators are single Unicode glyphs. To allow whitespace to be omitted wherever feasible, there are several rules for what will constitute a single identifier.

• An identifier can never contain a reserved character under any circumstances. These characters are treated specially by the lexer and parser.

• An identifier can consist of any string of non-reserved non-quoting characters surrounded by a pair of quoting characters. Most quoting brackets have specific purposes, and all quoting brackets are reserved:

  • The ornate brackets ﴾ and ﴿ are used to refer to identifiers that are Corbenic primitives. Defining your own is not permitted, and which primitives are avaliable will depend on the backend of choice (though most will be avaliable everywhere). Note that these make meaningfully different identifiers: ﴾x﴿ and x are not the same.

    • Example: ﴾+ℤℤ﴿, the primitive for addition of integers.

  • Guillemets « and » are used for two general purposes:

    • To explicitly mark that the containing characters should be treated as a single identifier.

      • Example: «+++» is a single identifier, +++ is a sequence of three instances of + (and will fail at parse time).
      • Note that unlike the ornate brackets, guillemets do not create new identifiers. «+» is the same as the + in the Prelude, and is the intended means to access Prelude’s addition as a value.

    • To use an identifier that has been declared with fixity as a standard value.

      • Example: 2 + 4 uses + infix, «+» 2 4 is semantically identical but uses + as a standard function.

• An identifier can consist of a capital letter (among the twenty-six Latin letters) in a given class followed by any number of letters in that same class. The classes are standard Latin letters alongside the various modifications present in the Unicode block Mathematical Alphanumeric Symbols.

  • Monoid, HasComplexUnit, ℕ, 𝕆𝕟, and 𝖃𝖞𝖟 are all single identifiers. 𝕆𝕟𝖃𝖞𝖟 is two, since the letters do not come from the same class.
• Unicode characters considered “space” characters ( , ZWSP, etc) are not legal in identifiers unless quoted (though they are not reserved). These characters terminate identifiers, but they are otherwise insignificant.

• Certain characters cannot stand as identifiers by themselves, but can be suffixed to an identifier to produce another identifier:

  • Exactly one instance of ⌞ or ⌟. These are commonly used where suffixing l or r would be done in Haskell. x⌟ is one identifier.
  • Any sequence of subscripted digits (₀₁₂₃₄₅₆₇₈₉) that does not begin with a leading ₀, except that a lone ₀ is legal. These subscripted digits are Corbenic’s way to get numbers into identifier names when they’re genuinely useful: SHA₂₅₆ is one identifier naming SHA-256, and operations on Bifunctors are often defined with the same glyphs as the corresponding operations on Functors suffixed with ₂.
  • Any of the prime characters: ′, ″, ‴, ‵, ‶, ‷
  • The subscript infinity ͚.
  • The superscript capital B 𐞄. (This is used for the fixed width integer and natural types.)
  • The superscript plus and minus ⁺ and ⁻
  • The complement symbol ∁ (commonly seen in operations involving contravariant functors)
• Characters used for quoting literals are reserved. These are ' for character literals, " for text literals, and [ and ] for list terms and types.
• Parentheses ( and ) are reserved (for grouping).
• The character ⍝ is used to begin comments and is thus reserved.
• Digits 0123456789 are reserved for numeric literals.
• The character ⏎ is reserved and is equivalent to a newline, with one exception: the number of spaces after a ⏎ does not affect the indentation level (see the section on Blocks below).

• Any single non-reserved character not covered by these rules is an identifier.

  • Examples: +, π, and ꙮ, f+, and xyz are all sequences of one-character identifiers.

Declarations

Corbenic has multiple types of declarations. To distinguish between declarations, different binding symbols are used.

• Term declarations are made using the ≔ symbol, which is reserved. x ≔ 2 is a term declaration.

• Type annotations are written using the reserved symbol ⠛. A type annotation for a declaration must be on the line immediately preceeding the declaration: x ⠛ ℤ on its own line, then x ≔ … below. Within a type expression itself, ⠛ is used infix as usual (⦿⌟₆ + ⠛ ∀x. x → x → x), and constraint notation (x ⋹ Additive ⇒ …) may appear anywhere a type can.

  • Type variables are never implicit. It is forbidden to write f ⠛ x → x → x, you must either explicit qualify it with ∀: f ⠛ ∀x. x → x → x or include it as a parameter in your declaration.

• Typeclass declarations are made using the symbol ⇒.

  • Constraints can be written in a standard form, such as (Functor x, Foldable x) ⇒ Traversable x, or they can be written in a set-algebra like form, as follows: x ⋹ Functor ⋒ Foldable.
  • Typeclasses with no constraints are declared with nothing before ⇒. For example, ⇒ Magma x on its own line is a legal typeclass definition.
  • Multiparameter typeclasses can also be declared using the set notation, put each parameter before the ⋹, like so: x y ⋹ Convertible
  • Set notation is also valid inside standard tuple notation to declare multiple constraints at once and still allow compression of common types, like so: (x ⋹ Foo ⋒ Bar, y ⋹ Baz)
  • Typeclass methods are declared in a block immediately following the declaration.
  • Typeclass blocks can also include associated types. To declare an associated type, begin the line with ≋ and then write the type before it. If you wish to include a default instantiation, put it after the ≋
  • Typeclass instance declarations are made with the ∴ character. Methods and associated types are declared in the same way as top level term declarations. For example, the head of an instance for Additive will look like this: ∴ Additive x or ∴ x ⋹ Additive

• Constraint aliases are declared with the reserved symbol ≣. These are methodless typeclasses which are aliases for a set of constraints and should be used only when there is no law associated with the class beyond merely satisfying the constraints.

  • Example: Since the typeclass Group demands only that its members are Associative, Unital, and Invertible, we define it like so: a ⋹ Group ≣ a ⋹ Associative ⋒ Unital ⋒ Invertible. However, Associative itself, despite having no methods beyond its constituent Magma, demands an additional law (associativity) and hence it must be declared explicitly using ⇒, like so: a ⋹ Magma ⇒ a ⋹ Associative. Note the reversal of order in the two cases.
• Type aliases are declared with the reserved symbol ≘. This corresponds to the type operator in Haskell and is a transparent expansion.
• General ADT Declarations are done using the reserved symbol ≗. Constructors are separated by the reserved character ¦. An example declaration is the Rose tree: Rose a ≗ Leaf a ¦ Tree [Rose a]
• Newtypes are declared with the reserved symbol ≛. An example declaration is the Identity monad: Identity a ≛ Identity a

• Fixity Declarations work differently from how they work in Haskell. In Corbenic, a fixity declaration is attached to the binding at declaration, and this is the only way to declare fixities. To declare fixity, prepend the name in the declaration with the reserved symbol ⦿ (which is the fixity declarator), followed by one of the following:

  • For right-associative binary operators, add ⌟ followed by the precedence as a subscripted number.
  • For left-associative binary operators, add ⌞ followed by the precedence, again as a subscripted number.
  • For non-associative binary operators, add only the precedence, again as a subscripted number.
  • For prefixed unary operators, add ⟓ followed by the precedence, again as a subscripted number.
  • For postfixed unary operators, add Ŀ followed by the precedence, again as a subscripted number.
  • Other than being a natural number, there is no restriction on precedence level, though it is recommended for most users to keep their precedences in the range zero to nine unless there is a pressing reason to do otherwise.
  • All unary operations bind tighter than all binary operations. Unary operations of the same precedence currently associate to the left, but this might change in a future version, so try not to rely on that behavior.

The following are the full definitions of the Additive and Multiplicative typeclasses to demonstrate the various declaration features:

⇒ Additive x
  ⦿⌟₆ + ⠛ x → x → x
  ⓪ ⠛ x

⇒ Multiplicative x
  ⦿⌟₅ * ⠛ x → x → x
  ① ⠛ x

Note that if you inspect the type of + in the REPL with :i +, you will see its type and fixity as ⦿⌟₆ + ⠛ ∀x. x ⋹ Additive ⇒ x → x → x. The implicit constraint is made explicit.

Comments

In Corbenic, comments begin with the character ⍝. If a comment begins with two copies of this character, ⍝⍝, it is a documentation comment. Documentation comments in the Prelude will be rendered on this site alongside the declarations of the various types and classes in Prelude. A documentation comment must immediately precede its declaration, or begin the module (for a module-wide comment). A mid-line documentation comment is a warning.

Blocks

Blocks in Corbenic are delineated by indentation. Exactly two spaces at the beginning of a line mark one indentation block. Corbenic uses blocks in several ways:

Pattern Matching - 🝡 Blocks

The 🝡 glyph is used to begin a pattern matching context. This is as most functional programming languages, with the expected glyphification:

«factorial» ⠛ ℕ → ℕ
«factorial» x ≔ 🝡x
  0 ↦ 1
  n ↦ n * «factorial» (n ∸ 1) ⍝ ∸ "monus" is subtraction but if a > b then b ∸ a is 0

Corbenic also supports using seqeuence λ🝡 to represent a lambda expression that immediately pattern matches on its argument:

«factorial» ≔ λ🝡
  0 ↦ 1
  n ↦ n * «factorial» (n ∸ 1)

Do Notation - 🝣 Blocks

Like Haskell, Corbenic has a form of do notation as syntactic sugar for monadic computations:

🝣
  x ↤ «foo»
  y ≔ bar
  «doSomethingMonadic» x y
  ☉ z     ⍝ on Applicatives, ☉ is Haskell's "pure"

Typeclass Blocks

Both the declaration of a typeclass and its instances are followed with all relevant methods in a block after the declaration (see the Additive and Multiplicative examples above)

Local Binding - Unmarked Blocks

A block in any other context is Corbenic’s method of scoped binding (like let or where). This is the only method of doing such a bind:

«foo» a b c ≔ «bar» x y z
  x ≔ «baz» a b
  y ≔ «quux» b c
  z ≔ «fingore» x y ⍝ local bindings can refer to each other!

Modules, Imports, and Exports

Corbenic has a module system. All files must begin with a module declaration, which is, on the first line,

▣ ModuleName

Module names must be standard Latin characters, and the opening square is a reserved character. Unlike Haskell, you do not specify the export list at the top of the file, but rather every declaration is assumed to be exported unless it is preceeded with the (reserved) character ※, in which case it is hidden.

The following declaration types can be marked hidden:

• Top level term declarations, type declarations (alias, newtype, data, or constraint aliases)
• Type constructors of newtype or data declarations

To import a module, use the reserved ⇲ glyph:

⇲ Foo.Bar

This will search, relative to the main module, for Foo/Bar.corb as the imported module. If you wish to import only certain things, list those imports in a block after the import:

⇲ Foo.Bar
  Baz
  Quux

alternatively, you can import everything except some set by prefixing each line in the block with ※:

⇲ Foo.Bar
  ※ Baz
  ※ Quux

Mixing both ※-prefixed lines and normal lines is permissible, but a warning (as the explicit exclusions are redundant).

All imported bindings will be in scope for the entire module. To qualify these imports, use the reserved ⌸ glyph:

⇲ Foo.Bar ⌸ T
  Baz
  Quux

will put the bindings in scope as T.Baz and T.Quux. If no name is specified after the ⌸, the bindings are qualified by the module name, e.g Foo.Bar.Baz.

If you wish to re-export this module, you need to specify that with the reserved ⇱ glyph:

⇱ Foo.Bar

which will by default re-export all bindings from that module which were imported. This set can be restricted further using the same block format as used when importing a module.

The Type System

Corbenic’s type system has the following features for both richness and quality of life. Several of these are based on their equivalent Haskell extensions, but are turned on by default:

Type Lambdas and Applications

The language has first class type lambdas and type aplications. To write a type lambda, use the reserved capital lambda: Λτ. <body>. Within the body of this expression, τ will be avaliable as a type variable.

To apply a type, wrap it in angle brackets 〈 and 〉. This is not restricted to explicitly defined type lambdas. You can also use this to constrain the types of polymorphic functions or typeclass methods (the latter is quite useful if type inference can’t determine which type you’re referring to).

• Example: If you wish to restrict the type of the identity function so that it will only work on natural numbers, you may write 𝟏 〈ℕ〉 which will have type ℕ → ℕ.

The Monomorphism Restriction

There isn’t one (as of now).

In Corbenic, all terms are generalized as much as they can be. Universally quantified types can be instantiated with different types in general. As always, type signatures can be used to change this behavior if you so desire.

Do beware, though. If you ever find the need to use a certain extremely dangerous function that gives an escape hatch out of the IO monad ⌘:

«☠⌘» ⠛ ∀a. ⌘ a → a

You are liable to duplicate IO actions. You (hopefully) already know what you’re doing if you want to reach for this, so the onus is on you to be safe.

Note: This is subject to change in the distant future when GADTs arrive, but even then what bars generalization will be quite limited.