Protocol Documentation

Table of Contents

• lang.proto

  • ClassConstraint

  • ClassDef

  • ClassName

  • ConstrName

  • Constraint

  • Derive

  • FieldName

  • InstanceClause

  • Kind

  • Kind.KindArrow

  • Module

  • ModuleName

  • ModuleNamePart

  • Opaque

  • Product

  • Record

  • Record.Field

  • SourceInfo

  • SourcePosition

  • Sum

  • Sum.Constructor

  • Ty

  • TyAbs

  • TyApp

  • TyArg

  • TyBody

  • TyClassRef

  • TyClassRef.Foreign

  • TyClassRef.Local

  • TyDef

  • TyName

  • TyRef

  • TyRef.Foreign

  • TyRef.Local

  • TyVar

  • Tys

  • VarName

  • Kind.KindRef

• compiler.proto

  • Error
  • Input
  • InternalError
  • KindCheckError
  • KindCheckError.CyclicKindError
  • KindCheckError.InconsistentTypeError
  • KindCheckError.UnboundTyRefError
  • KindCheckError.UnboundTyVarError
  • KindCheckError.UnificationError
  • NamingError
  • Output
  • ProtoParseError
  • ProtoParseError.MultipleClassDefError
  • ProtoParseError.MultipleConstructorError
  • ProtoParseError.MultipleFieldError
  • ProtoParseError.MultipleImportError
  • ProtoParseError.MultipleModuleError
  • ProtoParseError.MultipleTyArgError
  • ProtoParseError.MultipleTyDefError
  • ProtoParseError.OneOfNotSetError
  • ProtoParseError.UnknownEnumError
  • Result
  • TyClassCheckError
  • TyClassCheckError.DeriveOpaqueError
  • TyClassCheckError.ImportNotFoundError
  • TyClassCheckError.MissingRuleError
  • TyClassCheckError.OverlappingRulesError
  • TyClassCheckError.OverlappingRulesError.QHead
  • TyClassCheckError.SuperclassCycleError
  • TyClassCheckError.UnboundClassRefError

• codegen.proto

  • Error
  • Input
  • InternalError
  • Output
  • Result
  • UnsupportedClassError
  • UnsupportedOpaqueError

• Scalar Value Types

Top

lang.proto

ClassConstraint

Class constraints

A special constraint type denoting the constraints that occur on the rhs of class definitions. Only used to specify super class constraints in a ClassDef.

Not to be confused with Constraint which denote type class rules.

ClassDef

Type class definition

LambdaBuffers use type classes to talk about the various 'meanings' or 'semantics' we want to associate with the types in LambdaBuffers schemata.

For instance, most types can have Eq semantics, meaning they can be compared for equality. Other can have Ord semantics, meaning they can be ordered.

Using type classes and instance declarations, much like in Haskell, users can specify the 'meaning' of each type they declare. For example, serialization in LambdaBuffers is just another type class, it's treated the same as any other type class. Concretely, if we wish to provide JSON serialization for LambdaBuffers types, we declare such a type class and provide desired semantic rules:

module Foo

class JSON a

sum Foo a b = Bar a | Baz b

derive JSON (Foo a b)

Note that for each type class introduced, the Codegen machinery must be updated to support said type class. In other words, it doesn't come for free and for each new type class, a Codegen support must be implemented for any InstanceClause declared by the user. Once all the InstanceClauses have an implementation provided, all the Derived implementation come for free.

ClassName

Type class name

ConstrName

Sum type constructor name

Constraint

Constraint term

Derive

Derive statement

Derive statements enable user to specify 'semantic' rules for their types much like InstanceClauses do. However, the Codegen will be able to derive an implementation for any such constraint.

module Prelude

class Eq a

sum Maybe a = Just a | Nothing

derive Eq (Maybe a)

The rule installed for the derive statement is:

eq(maybe(A)) :- eq(just(A) | Nothing).

The rule relates the desired Ty term to its (lambda calculus) 'evaluated' form.

> Currently, there's only support for deriving type class rules and implementations for Ty terms of Kind.KIND_REF_TYPE. That means, type classes like Ord and Eq...

FieldName

Record type field name

InstanceClause

Instance clause

Instance clauses enable users to specify ad-hoc 'semantic' rules for their types. Each such instance must be supported explicitly in the Codegen by providing runtime implementations.

This rule form is used when declaring 'opaque' implementations on Opaque types.

module Prelude

class Eq a

opaque Maybe a

instance Eq a => Eq (Maybe a)

The rule installed for the clause is:

eq(maybe(A)) :- eq(A).

The instance clause is verbatim added to the rule set.

Kind

Kinds

A type of a type is called a 'kind'. In Lambda Buffers, all type terms, namely TyArg, TyVar, TyRef, TyApp and TyAbs, are either of kind Type or Type -> Type and Type -> Type -> Type etc.

Kind.KindArrow

A kind arrow.

Module

Module

A module encapsulates type, class and instance definitions.

ModuleName

Module name

ModuleNamePart

Module name part

Opaque

Opaque type.

A type that has an Opaque body represents a 'built-in' or a 'primitive' type that's handled by the semantics 'under the hood'. It's called 'opaque' to denote the fact that the Compiler has no knowledge of its structure, and relies that the necessary knowledge is implemented elsewhere. The Codegen modules for any target language have to be able to handle such types specifically and map to existing value level representations and corresponding types.

Codegen modules would have to implement support for such defined types, for example:

• In Python Set a would map to set() from the standard library,
• In Haskell Set a would map to containers.Data.Set.Set type.

Every Opaque type has to be considered deliberately for each language environment targeted by Codegen modules.

TODO(bladyjoker): Consider attaching explicit Kind terms to Opaques.

Product

A product type term.

Record

A record type term.

Record.Field

Field in a record type.

SourceInfo

Frontend Source information

Frontends are advised to include Source information to denote how their Source* content maps to the Compiler Input. It's essential when reporting Compiler* errors back to the Frontend.

SourcePosition

Position in Source

Sum

A sum type term.

A type defined as a Sum type is just like a Haskell algebraic data type and represents a sum of products.

Sum.Constructor

Constructor of a Sum type is a Product type term.

Ty

Type term

A type term that occurs in bodies of type definitions (message TyDef):

sum Maybe a = Just a | Nothing

sum Either a b = Left a | Right b

sum SomeType a = Foo a (Maybe a) | Bar (Either (Maybe a) (SomeType a))

or in instance declarations:

instance Eq (Maybe a)

instance Eq (SomeType Int)

instance (Eq (Maybe a), Eq (SomeType a)) Eq (Either (Maybe a) (SomeType a))

Check out examples.

TyAbs

Type abstraction

A type term that introduces type abstractions (ie. type functions). This type term can only be introduced in the context of a [type definition](@ref TyDef).

TyApp

Type application

A type term that applies a type abstraction to a list of arguments.

TyArg

Type arguments

Arguments in type abstractions.

Type arguments and therefore type variables have kinds, the Compiler only accepts Type kinded type arguments ans therefore type variables.

However, to allow for future evolution if ever necessary, we attach the Kind term to type arguments, even though the Compiler will reject any TyArg that's not of kind Type.

Note, this effectively means that lambda Buffers doesn't support higher-kinded types (ie. HKT).

TyBody

Type body.

Lambda Buffers type bodies type terms that can only be specified in the TyAbs context. It's a built-in type term that can only occur enclosed within a TyAbs term which introduces TyVars in the scope of the term.

TyClassRef

Type class references

It is necessary to know whether a type class is defined locally or in a foreign module when referring to it in a constraint, this allows users (and requires the frontend) to explicitly communicate that information.

TyClassRef.Foreign

Foreign class reference.

TyClassRef.Local

Local type reference.

TyDef

Type definition

A type definition consists of a type name and its associated type term.

One way to look at it is that a type definition introduces a named 'type abstraction' in the module scope. Concretely, Either can be considered a type lambda of kind Type -> Type -> Type.

In fact, type definitions are the only way to introduce such types.

Once introduced in the module scope, type definitions are referred to using [TyRef](@ref TyRef) term.

TyName

Type name

TyRef

Type reference

A type term that denotes a reference to a type available that's declared locally or in foreign modules.

TyRef.Foreign

Foreign type reference.

TyRef.Local

Local type reference.

TyVar

Type variable

Tys

A list of type terms useful for debugging

VarName

Type variable name

Kind.KindRef

A built-in kind.

Top

compiler.proto

Error

Compiler Error

Input

Compiler Input

Compiler Input is a fully self contained list of modules, the entire compilation closure needed by the Compiler to perform its task.

InternalError

Errors internal to the implementation.

KindCheckError

Kind checking errors.

KindCheckError.CyclicKindError

A cyclic kind was encountered. Infinite kinds like this are not acceptable, and we do not support them. We could not construct infinite kind in ty_def.

As the implementation currently stands such an error is (most likely) not representable - therefore not reachable. Such an error would usually occur for a term like: λa. a a - in which case the inference would try to unify two kinds of the form: m and m -> n - because m appears in both terms - the cyclic unification error would be thrown.

In the case of LambdaBuffers - such an error is not (currently) achievable as the kind of the variable is given by the context - (i.e. λa : m . a a, where m is a kind) therefore the unification would fail with Unification Error. Nevertheless - future features might require it.

KindCheckError.InconsistentTypeError

The actual_kind differs from the expected_kind.

KindCheckError.UnboundTyRefError

Unbound type reference ty_ref detected in term ty_def.

KindCheckError.UnboundTyVarError

Unbound variable ty_var detected in term ty_def.

KindCheckError.UnificationError

In ty_def an error has occurred when trying to unify kind ty_kind_lhs with ty_kind_rhs.

FIXME(cstml): Add source of constraint to the error such that user can see where the constraint was generated - therefore where the error precisely is.

NamingError

Naming error message

Output

Output of the Compiler.

ProtoParseError

All errors that occur because of Google Protocol Buffer's inability to enforce certain invariants. Some of invariance:

• using Proto map restricts users to string keys which impacts API documentation, which is why repeated fields are used throughout,
• using Proto 'oneof' means users have to check if such a field is set or report an error otherwise.

ProtoParseError.MultipleClassDefError

Multiple ClassDefs with the same ClassName were found in ModuleName.

ProtoParseError.MultipleConstructorError

Multiple Sum Constructors with the same ConstrName were found in ModuleName.TyDef.

ProtoParseError.MultipleFieldError

Multiple Record Fields with the same FieldName were found in ModuleName.TyDef.

ProtoParseError.MultipleImportError

ProtoParseError.MultipleModuleError

Multiple Modules with the same ModuleName were found.

ProtoParseError.MultipleTyArgError

Multiple TyArgs with the same ArgName were found in ModuleName.TyDef.

ProtoParseError.MultipleTyDefError

Multiple TyDefs with the same TyName were found in ModuleName.

ProtoParseError.OneOfNotSetError

Proto oneof field is not set.

ProtoParseError.UnknownEnumError

Proto enum field is unknown.

Result

Compiler Result ~ a successful Compilation Output.

TyClassCheckError

Type class checking errors.

TyClassCheckError.DeriveOpaqueError

In module_name it wasn't possible to solve constraint because a sub_constraint has been derived on an Opaque type. Opaque type can only have an InstanceClause declared for them.

TyClassCheckError.ImportNotFoundError

Import missing wasn't found in module_name

TyClassCheckError.MissingRuleError

In module_name while trying to solve constraint it wasn't possible to find a rule (Derive or InstanceClause) for sub_constraint.

TyClassCheckError.OverlappingRulesError

In module_name while trying to solve constraint overlaps (Derive or InstanceClause) were found that could be used to solve the sub_constraint.

TyClassCheckError.OverlappingRulesError.QHead

NOTE(bladyjoker): This should rather be oneof Derive and InstanceClause.

TyClassCheckError.SuperclassCycleError

Superclass cycle cycled_class_refs was detected when checking a class definition for class_name in module module_name.

TyClassCheckError.UnboundClassRefError

Unbound class_ref detected in module_name.

Top

codegen.proto

Error

Codegen Error

Input

Codegen Input

Codegen Input is a fully self contained list of modules, that have been checked by the Compiler.

InternalError

Errors internal to the implementation.

Output

Codegen output.

Result

Codegen Result ~ a successful Codegen Output.

UnsupportedClassError

Unsupported Class error for a class class_name defined in module module_name.

UnsupportedOpaqueError

Unsupported Opaque error for a type ty_name defined in module module_name.

Scalar Value Types