package lambdabuffers

Get desktop application:
View/edit binary Protocol Buffers messages

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.

Used in: ClassDef

• optional TyClassRef class_ref = 1

  Type class reference.

• repeated TyVar args = 2

  Type variables quantified over `ClassDef` arguments.

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: ```lbf 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 `InstanceClause`s have an implementation provided, all the `Derive`d implementation come for free.

Used in: Module, compiler.ProtoParseError.MultipleClassDefError

• optional ClassName class_name = 1

  Type class name.

• repeated TyArg class_args = 2

  Type class arguments. Class with no arguments is a trivial class. Compiler MAY report an error. TODO(bladyjoker): MultipleClassArgError.

• repeated ClassConstraint supers = 3

  Superclass constraints.

• string documentation = 4

  Documentation elaborating on the type class.

• optional SourceInfo source_info = 5

  Source information.

Type class name

Used in: ClassDef, TyClassRef.Foreign, TyClassRef.Local, codegen.UnsupportedClassError, compiler.NamingError, compiler.TyClassCheckError.SuperclassCycleError

• string name = 1

  Name ::= [A-Z]+[A-Za-z0-9_]*

• optional SourceInfo source_info = 2

  Source information.

Sum type constructor name

Used in: Sum.Constructor, compiler.NamingError

• string name = 1

  Name ::= [A-Z]+[A-Za-z0-9_]*

• optional SourceInfo source_info = 2

  Source information.

Constraint term

Used in: Derive, InstanceClause, compiler.TyClassCheckError.DeriveOpaqueError, compiler.TyClassCheckError.MissingRuleError, compiler.TyClassCheckError.OverlappingRulesError, compiler.TyClassCheckError.OverlappingRulesError.QHead

• optional TyClassRef class_ref = 1

  Name of the type class.

• repeated Ty args = 2

  Constraint arguments. Constraint with no arguments is a trivial constraint. Compiler MAY report an error.

• optional SourceInfo source_info = 3

  Source information.

Derive statement Derive statements enable user to specify 'semantic' rules for their types much like `InstanceClause`s do. However, the Codegen will be able to derive an implementation for any such constraint. ```lbf module Prelude class Eq a sum Maybe a = Just a | Nothing derive Eq (Maybe a) ``` The rule installed for the derive statement is: ```prolog 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...

Used in: Module

• optional Constraint constraint = 1

  Constraint to derive.

Record type field name

Used in: Record.Field, compiler.NamingError

• string name = 1

  Name ::= [a-z]+[A-Za-z0-9_]*

• optional SourceInfo source_info = 2

  Source information.

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. ```lbf module Prelude class Eq a opaque Maybe a instance Eq a => Eq (Maybe a) ``` The rule installed for the clause is: ```prolog eq(maybe(A)) :- eq(A). ``` The instance clause is verbatim added to the rule set.

Used in: Module

• optional Constraint head = 1

  Head of the clause that holds only when the `body` holds. Type variables introduced in the head of the rule become available in the scope of the body of the rule.

• repeated Constraint constraints = 3

  Instance (rule) body, conjunction of constraints.

• optional SourceInfo source_info = 4

  Source information.

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.

Used in: Kind.KindArrow, TyArg, compiler.KindCheckError.InconsistentTypeError, compiler.KindCheckError.UnificationError

• oneof kind

  Kind built-in reference or a kind arrow.

  • Kind.KindRef kind_ref = 1

  • Kind.KindArrow kind_arrow = 2

A kind arrow.

Used in: Kind

• optional Kind left = 1

• optional Kind right = 2

A built-in kind.

Used in: Kind

• KIND_REF_UNSPECIFIED = 0

  Unspecified kind SHOULD be inferred by the Compiler.

• KIND_REF_TYPE = 1

  A `Type` kind (also know as `*` in Haskell) built-in.

Module A module encapsulates type, class and instance definitions.

Used in: codegen.Input, compiler.Input, compiler.ProtoParseError.MultipleModuleError

• optional ModuleName module_name = 1

  Module name.

• repeated TyDef type_defs = 2

  Type definitions. Duplicate type definitions MUST be reported with `ProtoParseError.MultipleTyDefError`.

• repeated ClassDef class_defs = 3

  Type class definitions. Duplicate class definitions MUST be reported with `ProtoParseError.MultipleClassDefError`.

• repeated InstanceClause instances = 4

  Type class instance clauses.

• repeated Derive derives = 5

  Type class derive statements.

• repeated ModuleName imports = 6

  Imported modules the Compiler consults when searching for type class rules. TODO(bladyjoker): Rename to ruleImports. Duplicate imports MUST be reported with `ProtoParseError.MultipleImportError`.

• optional SourceInfo source_info = 7

  Source information.

Module name

Used in: Module, TyClassRef.Foreign, TyRef.Foreign, codegen.UnsupportedClassError, codegen.UnsupportedOpaqueError, compiler.KindCheckError.CyclicKindError, compiler.KindCheckError.InconsistentTypeError, compiler.KindCheckError.UnboundTyRefError, compiler.KindCheckError.UnboundTyVarError, compiler.KindCheckError.UnificationError, compiler.ProtoParseError.MultipleClassDefError, compiler.ProtoParseError.MultipleConstructorError, compiler.ProtoParseError.MultipleFieldError, compiler.ProtoParseError.MultipleImportError, compiler.ProtoParseError.MultipleTyArgError, compiler.ProtoParseError.MultipleTyDefError, compiler.TyClassCheckError.DeriveOpaqueError, compiler.TyClassCheckError.ImportNotFoundError, compiler.TyClassCheckError.MissingRuleError, compiler.TyClassCheckError.OverlappingRulesError, compiler.TyClassCheckError.OverlappingRulesError.QHead, compiler.TyClassCheckError.SuperclassCycleError, compiler.TyClassCheckError.UnboundClassRefError

• repeated ModuleNamePart parts = 1

  Parts of the module name denoting a hierarchical namespace.

• optional SourceInfo source_info = 2

  Source information.

Module name part

Used in: ModuleName, compiler.NamingError

• string name = 1

  Name ::= [A-Z]+[A-Za-z0-9_]*

• optional SourceInfo source_info = 2

  Source information.

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.

Used in: TyBody

• optional SourceInfo source_info = 1

  Source information.

A product type term.

Used in: Sum.Constructor, TyBody

• repeated Ty fields = 1

  Fields in a products are types.

• optional SourceInfo source_info = 2

  Source information.

A record type term.

Used in: TyBody

• repeated Record.Field fields = 1

  Record fields.

• optional SourceInfo source_info = 2

  Source information.

Field in a record type.

Used in: Record, compiler.ProtoParseError.MultipleFieldError

• optional FieldName field_name = 1

  Record field name.

• optional Ty field_ty = 2

  Field type.

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.

Used in: ClassDef, ClassName, ConstrName, Constraint, FieldName, InstanceClause, Module, ModuleName, ModuleNamePart, Opaque, Product, Record, Sum, TyAbs, TyApp, TyArg, TyClassRef.Foreign, TyClassRef.Local, TyDef, TyName, TyRef.Foreign, TyRef.Local, VarName, codegen.InternalError, compiler.InternalError

• string file = 1

  A filename denoting the Source file.

• optional SourcePosition pos_from = 2

  Starting position in Source.

• optional SourcePosition pos_to = 3

  End position in Source.

Position in Source

Used in: SourceInfo

• int32 column = 1

  Column index in the Source.

• int32 row = 2

  Row index in the Source.

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.

Used in: TyBody

• repeated Sum.Constructor constructors = 1

  Sum type constructors. Empty `constructors` means `void` and means that the type can't be constructed. Compiler MAY report an error. Duplicate constructors MUST be reported with `ProtoParseError.MultipleConstructorError`.

• optional SourceInfo source_info = 2

  Source information.

Constructor of a Sum type is a Product type term.

Used in: Sum, compiler.ProtoParseError.MultipleConstructorError

• optional ConstrName constr_name = 1

  Constructor name.

• optional Product product = 2

  Product type term.

Type term A type term that occurs in bodies of type definitions (message TyDef): ```lbf 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: ```lbf instance Eq (Maybe a) instance Eq (SomeType Int) instance (Eq (Maybe a), Eq (SomeType a)) Eq (Either (Maybe a) (SomeType a)) ``` Check out [examples](examples/tys.textproto).

Used in: Constraint, Product, Record.Field, TyApp, Tys

• oneof ty

  A type variable, a type reference or a type application.

  • TyVar ty_var = 1

    A type variable.

  • TyApp ty_app = 2

    A type application.

  • TyRef ty_ref = 3

    A type reference.

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).

Used in: TyDef

• repeated TyArg ty_args = 1

  List of type variables. No type arguments means `delay` or `const ty_body`, meaning `TyAbs [] ty_body = ty_body`. Duplicate type arguments MUST be reported with `ProtoParseError.MultipleTyArgError`.

• optional TyBody ty_body = 2

  Type body.

• optional SourceInfo source_info = 3

  Source information.

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

Used in: Ty

• optional Ty ty_func = 1

  Type function. TODO(bladyjoker): Rename to ty_abs?

• repeated Ty ty_args = 2

  Arguments to apply. No arguments to apply means `force`, meaning `TyApp ty_func [] = ty_func``

• optional SourceInfo source_info = 3

  Source information.

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).

Used in: ClassDef, TyAbs, compiler.ProtoParseError.MultipleTyArgError

• optional VarName arg_name = 1

  Argument name corresponds to variable names.

• optional Kind arg_kind = 2

  Argument kind.

• optional SourceInfo source_info = 3

  Source information.

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 `TyVar`s in the scope of the term.

Used in: TyAbs

• oneof ty_body

  Either an opaque, a sum/product/record type term.

  • Opaque opaque = 1

  • Sum sum = 2

  • Product product = 3

  • Record record = 4

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.

Used in: ClassConstraint, Constraint, compiler.TyClassCheckError.SuperclassCycleError, compiler.TyClassCheckError.UnboundClassRefError

• oneof class_ref

  Local or a foreign type class reference.

  • TyClassRef.Local local_class_ref = 1

  • TyClassRef.Foreign foreign_class_ref = 2

Foreign class reference.

Used in: TyClassRef

• optional ClassName class_name = 1

  Foreign module class name.

• optional ModuleName module_name = 2

  Foreign module name.

• optional SourceInfo source_info = 3

  Source information.

Local type reference.

Used in: TyClassRef

• optional ClassName class_name = 1

  Local module class name.

• optional SourceInfo source_info = 2

  Source information.

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.

Used in: Module, compiler.KindCheckError.CyclicKindError, compiler.KindCheckError.InconsistentTypeError, compiler.KindCheckError.UnboundTyRefError, compiler.KindCheckError.UnboundTyVarError, compiler.KindCheckError.UnificationError, compiler.ProtoParseError.MultipleConstructorError, compiler.ProtoParseError.MultipleFieldError, compiler.ProtoParseError.MultipleTyArgError, compiler.ProtoParseError.MultipleTyDefError

• optional TyName ty_name = 1

  Type name.

• optional TyAbs ty_abs = 2

  Type term.

• optional SourceInfo source_info = 3

  Source information.

Type name

Used in: TyDef, TyRef.Foreign, TyRef.Local, codegen.UnsupportedOpaqueError, compiler.NamingError

• string name = 1

  Name ::= [A-Z]+[A-Za-z0-9_]*

• optional SourceInfo source_info = 2

  Source information.

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

Used in: Ty, compiler.KindCheckError.UnboundTyRefError

• oneof ty_ref

  Local or a foreign type reference.

  • TyRef.Local local_ty_ref = 1

  • TyRef.Foreign foreign_ty_ref = 2

Foreign type reference.

Used in: TyRef

• optional TyName ty_name = 1

  Foreign module type name.

• optional ModuleName module_name = 2

  Foreign module name.

• optional SourceInfo source_info = 3

  Source information.

Local type reference.

Used in: TyRef

• optional TyName ty_name = 1

  Local module type name.

• optional SourceInfo source_info = 2

  Source information.

Type variable

Used in: ClassConstraint, Ty, compiler.KindCheckError.UnboundTyVarError

• optional VarName var_name = 1

  Variable name.

A list of type terms useful for debugging

• repeated Ty ties = 1

Type variable name

Used in: TyArg, TyVar, compiler.NamingError

• string name = 1

  Name ::= [a-z]+

• optional SourceInfo source_info = 2

  Source information.