Skip to content

Instantly share code, notes, and snippets.

@brendanzab

brendanzab/ddl-experiment.makam

Last active May 11, 2020 05:30
Show Gist options
  • Save brendanzab/7a331adae167ef6399c6b762aa943abd to your computer and use it in GitHub Desktop.
Save brendanzab/7a331adae167ef6399c6b762aa943abd to your computer and use it in GitHub Desktop.
Download ZIP
A dependently typed binary data description language, prototyped in Makam!
Raw
ddl-experiment.makam
% Copyright 2020 YesLogic Pty. Ltd.
%
% Licensed under the Apache License, Version 2.0 (the "License");
% you may not use this file except in compliance with the License.
% You may obtain a copy of the License at
%
% http://www.apache.org/licenses/LICENSE-2.0
%
% Unless required by applicable law or agreed to in writing, software
% distributed under the License is distributed on an "AS IS" BASIS,
% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
% See the License for the specific language governing permissions and
% limitations under the License.
% A dependently typed binary data description language, prototyped in Makam!
%
% I'm experimenting with Makam as a way of prototyping ideas for my exisiting
% ddl implementation at https://github.com/yeslogic/ddl.
%
% Roadmap:
%
% - [ ] split specification into multiple files
% - [-] core language
% - [-] language feautures
% - [x] basic MLTT (without identity types)
% - [x] basic binary format descriptions
% - [ ] unions
% - [ ] refinement types
% - [ ] multi-stage programming
% - [x] normalization by evaluation
% - [-] declarative typing rules
% - [x] bidirectional type checking rules
% - [ ] binary format interpretation
% - [ ] bidirectional elaboration
% - [ ] compilation passes
% - [ ] stratified
% - [ ] unkinded
% - [ ] uncurried
% - [ ] rust
% Core language
%
% The core language is an extension of Martin-Löf type theory, with some builtin
% data types, like booleans, integers, and arrays, and support for defining
% binary format descriptions. We skip identity types and η-rules for now.
%
% In making this language, we owe much of our inspiration to the work on PADS/ML
% and the data description calculus (DDC) in ["The Next 700 Data Description Languages"].
% In contrast to DDC, we have decided to 'embed' format descriptions within a
% dependendently typed language rather than splitting the language up into
% separate format and host languages.
%
% At the moment it's possible to describe 'dependent format descriptions'. This
% could be useful for 'extensible' binary formats, but it makes compilation much
% harder. We might ultimately want to restrict this in the future for ease of
% compilation through some use of [multi-stage programming], either using an
% approach based on [modal type theory], or by 'intentionally' conflating
% 'phase' with 'universe level', as described in ["Phase Distinctions in Type Theory"].
%
% ["Phase Distinctions in Type Theory"]: http://lucacardelli.name/Papers/PhaseDistinctions.A4.pdf
% ["The Next 700 Data Description Languages"]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.1375
% [modal type theory]: https://jozefg.github.io/papers/2019-implementing-modal-dependent-type-theory.pdf
% [multi-stage programming]: https://github.com/metaocaml/metaocaml-bibliography
%extend core.
% Syntax
%
% This section defines the core syntax of the data description language.
%
% # A note on naming
%
% In general we try to keep to the following naming scheme:
%
% - `thing_type` describes the shape of some `thing`
% - `thing_intro` introduces an element of `thing_type`
% - `thing_elim` eliminates an element of `thing_type`
%
% Based on this naming-scheme, we follow this terminology mapping:
%
% | [Type theory] name | Our name |
% | ----------------------- | --------------------- |
% | [Pi type] | `function_type` |
% | [Lambda abstraction] | `function_intro` |
% | [Function application] | `function_elim` |
% | [Sigma type] | `pair_type` |
% | [Pairing] | `pair_intro` |
% | Project first | `pair_elim_first` |
% | Project second | `pair_elim_second` |
%
% [Type theory]: https://ncatlab.org/nlab/show/type+theory
% [Pi type]: https://ncatlab.org/nlab/show/dependent+product+type
% [Lambda abstraction]: https://ncatlab.org/nlab/show/lambda-abstraction
% [Function application]: https://ncatlab.org/nlab/show/function+application
% [Sigma type]: https://ncatlab.org/nlab/show/dependent+sum+type
% [Pairing]: https://ncatlab.org/nlab/show/pairing
%
% I'm not entirely sold on these suffixes - here are some alternatives that
% I've currently come up with:
%
% - `_type`, `_elem`, `_apply`
% - `_type`, `_elem`, `_call`
% - `_space`, `_point`, `_???`
%
% Let me know if you have other ideas!
%
% # An annoying naming issue
%
% I have `InputTerm : term` for a function argument, that then gets
% evaluated to `InputValue : value`. but then I have `InputType : term` for
% a parameter type... but I can't do `InputValue : value` - it's already
% taken for the term level! And I can't do `InputType : type` because that's
% taken by the term.
% Terms
term : type.
% Variables
local : int -> term. % Local variables (using De Bruijn indices)
% Annotated terms
ann : term -> term -> term.
% Universes
universe : term.
% Void
void_type : term.
% Unit
unit_type : term.
unit_intro : term.
% Functions
function_type : term -> term -> term. % Also known as: Pi type, Dependent product type
function_intro : term -> term. % Also known as: Lambda abstraction, anonymous function
function_elim : term -> term -> term. % Also known as: Function application
% Pairs
pair_type : term -> term -> term. % Also known as: Sigma type, Dependent sum type
pair_intro : term -> term -> term. % Also known as: Pair constructor
pair_elim_first : term -> term.
pair_elim_second : term -> term.
% Refinements
% refine_type : term -> term -> term.
% refine_intro : term -> (* some proof from a solver here? *) -> term.
% Staging
% stage_type : term -> term.
% stage_intro : term -> term.
% stage_elim : term -> term.
% Booleans
bool_type : term.
bool_intro : bool -> term.
bool_elim : term -> term -> term -> term.
% Integers
int_type : term.
int_intro : int -> term.
% Arrays
array_type : term -> term -> term.
array_intro : list term -> term.
array_elim : term -> term -> term.
% Binary format descriptions
format_type : term.
format_intro_void : term.
format_intro_unit : term.
format_intro_u8 : term.
format_intro_u16le : term. % TODO: make this a computed format?
format_intro_u16be : term. % TODO: make this a computed format?
format_intro_u32le : term. % TODO: make this a computed format?
format_intro_u32be : term. % TODO: make this a computed format?
format_intro_u64le : term. % TODO: make this a computed format?
format_intro_u64be : term. % TODO: make this a computed format?
format_intro_s8 : term. % TODO: make this a computed format?
format_intro_s16le : term. % TODO: make this a computed format?
format_intro_s16be : term. % TODO: make this a computed format?
format_intro_s32le : term. % TODO: make this a computed format?
format_intro_s32be : term. % TODO: make this a computed format?
format_intro_s64le : term. % TODO: make this a computed format?
format_intro_s64be : term. % TODO: make this a computed format?
format_intro_array : term -> term -> term.
format_intro_pair : term -> term -> term.
format_elim : term -> term.
% Items
item : type.
declaration : string -> term -> item.
definition : string -> term -> item.
%extend typing.
% Declarative Typing
%
% This section defines the typing rules in a way that is close to a
% standard presentation of Martin-Löf Type Theory with explicit
% substitutions. The disadvantage of this description is that it's hard
% to derive an actual type checker implementation directly from these
% rules. We instead to this later on, by describing a bidirectional type
% checking algorithm in the `core.typing.bidirectional` namespace.
% Further reading:
%
% - https://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf
% - http://www.cse.chalmers.se/research/group/logic/book/book.pdf
%extend declarative.
% Declarative typing context
context : type.
% Empty typing context
empty : context.
% A typing context, extended with a new binding
extend : context -> term -> context.
is_context : context -> prop.
is_type : context -> term -> prop.
is_elem : context -> term -> term -> prop.
% is_subst : context -> subst -> context -> prop.
is_equal_type : context -> term -> term -> prop.
is_equal_elem : context -> term -> term -> term -> prop.
% is_equal_subst : context -> subst -> subst -> context -> prop.
% Contexts
is_context empty.
is_context (extend Context Type) :-
is_context Context,
is_type Context Type.
% Reflexivity
is_equal_type Context Type Type :-
is_type Context Type.
is_equal_elem Context Term Term Type :-
is_type Context Type.
% Symmetry
is_equal_type Context Type1 Type2 :-
is_equal_type Context Type2 Type1.
is_equal_elem Context Term1 Term2 Type :-
is_equal_elem Context Term2 Term1 Type.
% Transitivity
is_equal_type Context Type1 Type3 :-
is_equal_type Context Type1 Type2,
is_equal_type Context Type2 Type3.
is_equal_elem Context Term1 Term3 Type :-
is_equal_elem Context Term1 Term2 Type,
is_equal_elem Context Term1 Term3 Type.
% Type Equality
is_elem Context Term Type2 :-
is_elem Context Term Type1,
is_equal_type Context Type1 Type2.
is_equal_elem Context Term1 Term2 Type2 :-
is_equal_elem Context Term1 Term2 Type1,
is_equal_type Context Type1 Type2.
% Variables
is_type (extend Context Type) (local 0) :-
is_type Context Type.
is_type (extend Context _) (local Index) :-
plus PrevIndex 1 Index,
is_type Context (local PrevIndex).
is_elem (extend Context Type') (local 0) Type :-
is_elem Context Type' Type.
is_elem (extend Context _) (local Index) Type :-
plus PrevIndex 1 Index,
is_elem Context (local PrevIndex) Type.
% Universes
is_type Context universe :-
is_context Context.
% Void
is_type Context void_type :-
is_context Context.
is_elem Context void_type universe :-
is_context Context.
% Unit
is_type Context unit_type :-
is_context Context.
is_elem Context unit_type universe :-
is_context Context.
is_elem Context unit_intro unit_type :-
is_context Context.
% Functions
is_type Context (function_type InputType OutputType) :-
is_type Context InputType,
is_type (extend Context InputType) OutputType.
is_elem Context (function_type InputType OutputType) universe :-
is_type Context InputType,
is_type (extend Context InputType) OutputType.
is_elem Context (function_intro OutputTerm) (function_type InputType OutputType) :-
is_type Context InputType,
is_elem (extend Context InputType) OutputTerm OutputType.
% is_elem Context (function_elim (function_intro OutputTerm) InputTerm) OutputType :- TODO.
% is_equal_elem Context (function_elim (function_intro OutputTerm) InputTerm) Term OutputType :- TODO.
% Pairs
is_type Context (pair_type FirstType SecondType) :-
is_elem Context FirstType universe,
is_elem (extend Context FirstType) SecondType universe.
is_elem Context (pair_type FirstType SecondType) universe :-
is_elem Context FirstType universe,
is_elem (extend Context FirstType) SecondType universe.
% is_elem Context (pair_intro FirstTerm SecondTerm) (pair_type FirstType SecondType) :- TODO.
% is_elem Context (pair_elim_first (pair_intro FirstTerm SecondTerm)) FirstType :- TODO.
% is_elem Context (pair_elim_second (pair_intro FirstTerm SecondTerm)) SecondType :- TODO.
% is_equal_elem Context (pair_elim_first (pair_intro FirstTerm SecondTerm)) Term FirstType :- TODO.
% is_equal_elem Context (pair_elim_second (pair_intro FirstTerm SecondTerm)) Term SecondType :- TODO.
% Booleans
is_type Context bool_type :-
is_context Context.
is_elem Context bool_type universe :-
is_context Context.
is_elem Context (bool_intro _) bool_type :-
is_context Context.
is_elem Context (bool_elim BoolTerm TrueTerm FalseTerm) Type :-
is_elem Context BoolTerm bool_type,
is_type Context Type,
is_elem Context TrueTerm Type,
is_elem Context FalseTerm Type.
is_equal_elem Context (bool_elim (bool_intro true) TrueTerm FalseTerm) TrueTerm Type :-
is_type Context Type,
is_elem Context TrueTerm Type,
is_elem Context FalseTerm Type.
is_equal_elem Context (bool_elim (bool_intro false) TrueTerm FalseTerm) FalseTerm Type :-
is_type Context Type,
is_elem Context TrueTerm Type,
is_elem Context FalseTerm Type.
% Integers
is_type Context int_type :-
is_context Context.
is_elem Context int_type universe :-
is_context Context.
is_elem Context (int_intro _) int_type :-
is_context Context.
% Arrays
is_type Context (array_type ElemType LenTerm) :-
is_elem Context ElemType universe,
is_elem Context LenTerm int_type.
is_elem Context (array_type ElemType LenTerm) universe :-
is_elem Context ElemType universe,
is_elem Context LenTerm int_type.
is_elem Context (array_intro ElemTerms) (array_type ElemType LenTerm) :-
is_equal_elem Context (int_intro Len) LenTerm int_type,
length ElemTerms Len,
map (fun elem_term => is_elem Context elem_term ElemType) ElemTerms.
is_equal_elem Context (array_elim (array_intro ElemTerms) IndexTerm) ElemTerm ElemType :-
% FIXME: ensure `IndexTerm` is in array bounds, possibly with refinement types?
is_equal_elem Context (int_intro Index) IndexTerm int_type,
map (fun elem_term => is_elem Context elem_term ElemType) ElemTerms,
list.nth ElemTerms Index ElemTerm.
% Binary format descriptions
is_type Context format_type :-
is_context Context.
is_elem Context format_intro_void format_type :-
is_context Context.
is_elem Context format_intro_unit format_type :-
is_context Context.
is_elem Context format_intro_u8 format_type :-
is_context Context.
is_elem Context format_intro_u16le format_type :-
is_context Context.
is_elem Context format_intro_u16be format_type :-
is_context Context.
is_elem Context format_intro_u32le format_type :-
is_context Context.
is_elem Context format_intro_u32be format_type :-
is_context Context.
is_elem Context format_intro_u64le format_type :-
is_context Context.
is_elem Context format_intro_u64be format_type :-
is_context Context.
is_elem Context format_intro_s8 format_type :-
is_context Context.
is_elem Context format_intro_s16le format_type :-
is_context Context.
is_elem Context format_intro_s16be format_type :-
is_context Context.
is_elem Context format_intro_s32le format_type :-
is_context Context.
is_elem Context format_intro_s32be format_type :-
is_context Context.
is_elem Context format_intro_s64le format_type :-
is_context Context.
is_elem Context format_intro_s64be format_type :-
is_context Context.
is_elem Context (format_intro_array ElemType LenTerm) format_type :-
is_elem Context ElemType format_type,
is_elem Context LenTerm int_type.
is_elem Context (format_intro_pair FirstType SecondType) format_type :-
is_elem Context FirstType format_type,
is_elem (extend Context (format_elim FirstType)) SecondType format_type.
is_equal_elem Context (format_elim format_intro_void) void_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_unit) unit_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u8) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u16le) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u16be) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u32le) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u32be) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u64le) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_u64be) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s8) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s16le) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s16be) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s32le) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s32be) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s64le) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim format_intro_s64be) int_type universe :-
is_context Context.
is_equal_elem Context (format_elim (format_intro_array ElemType LenTerm)) (array_type ElemType' LenTerm) format_type :-
is_equal_elem Context (format_elim ElemType) ElemType' universe.
% TODO: format_intro_pair
%end.
%end.
% Semantics
%
% This section defines an operational semantics for language, using
% normalization-by-evaluation for performance reasons.
%extend semantics.
% The result of evaluating a term.
value : type.
% Neutral values are computations that are currently 'stuck' on some
% as-yet unknown computation. We build up a 'spine' of eliminations
% that cannot yet reduce in preperation for if they become 'unstuck'.
neutral : type.
% Closures are terms from the core syntax that have yet to be evaluated.
% They capture an environment of values to be used later, when they are
% finally evaluated.
closure : type.
% Neutral values
neutral : neutral -> value.
% Universes
universe : value.
% Void
void_type : value.
% Unit
unit_type : value.
unit_intro : value.
% Functions
function_type : value -> closure -> value. % Also known as: Pi type, Dependent product type
function_intro : closure -> value. % Also known as: Lambda abstraction, anonymous function
% Pairs
pair_type : value -> closure -> value. % Also known as: Sigma type, Dependent sum type
pair_intro : value -> value -> value. % Also known as: Pair constructor
% Refinements
% refine_type : value -> closure -> value.
% refine_intro : value -> (* some proof from a solver here? *) -> value.
% Staging
% stage_type : value -> value.
% stage_intro : value -> value.
% Booleans
bool_type : value.
bool_intro : bool -> value.
% Integers
int_type : value.
int_intro : int -> value.
% Arrays
array_type : value -> value -> value.
array_intro : list value -> value.
% Binary format descriptions
format_type : value.
format_intro_void : value.
format_intro_unit : value.
format_intro_u8 : value.
format_intro_u16le : value.
format_intro_u16be : value.
format_intro_u32le : value.
format_intro_u32be : value.
format_intro_u64le : value.
format_intro_u64be : value.
format_intro_s8 : value.
format_intro_s16le : value.
format_intro_s16be : value.
format_intro_s32le : value.
format_intro_s32be : value.
format_intro_s64le : value.
format_intro_s64be : value.
format_intro_array : value -> value -> value.
format_intro_pair : value -> closure -> value.
% Variables
local : int -> neutral. % Local variables (using De Bruijn levels)
% Suspended eliminations
function_elim : neutral -> value -> neutral.
pair_elim_first : neutral -> neutral.
pair_elim_second : neutral -> neutral.
% stage_elim : neutral -> neutral.
% bool_elim : neutral -> value -> value -> neutral.
% array_elim : neutral -> value -> neutral.
format_elim : neutral -> neutral.
closure : list value -> term -> closure.
% Evaluation of terms into values
eval : list value -> term -> value -> prop.
apply : closure -> value -> value -> prop.
apply_param : closure -> int -> value -> prop.
function_elim : value -> value -> value -> prop.
pair_elim_first : value -> value -> prop.
pair_elim_second : value -> value -> prop.
% stage_elim : value -> value -> prop.
% bool_elim : value -> value -> value -> value -> prop.
% array_elim : value -> value -> value -> prop.
format_elim : value -> value -> prop.
eval Values (local Index) Value :-
list.nth Values Index Value.
eval Values (ann Term _) Value :-
eval Values Term Value.
eval Values universe universe.
eval Values void_type void_type.
eval Values unit_type unit_type.
eval Values unit_intro unit_intro.
eval Values (function_type InputType OutputType) (function_type InputType' (closure Values OutputType)) :-
eval Values InputType InputType'.
eval Values (function_intro OutputTerm) (function_intro (closure Values OutputTerm)).
eval Values (function_elim Term InputTerm) Value' :-
eval Values Term Value,
eval Values InputTerm InputValue,
function_elim Value InputValue Value'.
eval Values (pair_type FirstType SecondType) (pair_type FirstType' (closure Values SecondType)) :-
eval Values FirstType FirstType'.
eval Values (pair_intro FirstTerm SecondTerm) (pair_intro FirstValue SecondValue) :-
eval Values FirstTerm FirstValue,
eval Values SecondTerm SecondValue.
eval Values (pair_elim_first PairTerm) FirstValue :-
eval Values PairTerm PairValue,
pair_elim_first PairValue FirstValue.
eval Values (pair_elim_second PairTerm) SecondValue :-
eval Values PairTerm PairValue,
pair_elim_second PairValue SecondValue.
eval Values bool_type bool_type.
eval Values (bool_intro Bool) (bool_intro Bool).
% FIXME: This breaks for neutral terms! We should use `bool_elim` here.
eval Values (bool_elim BoolTerm TrueTerm _) Value :-
eval Values BoolTerm (bool_intro true),
eval Values TrueTerm Value.
eval Values (bool_elim BoolTerm _ False1Term) Value :-
eval Values BoolTerm (bool_intro false),
eval Values FalseTerm Value.
eval Values int_type int_type.
eval Values (int_intro Int) (int_intro Int).
eval Values (array_type ElemType LenTerm) (array_type ElemType' LenValue) :-
eval Values ElemType ElemType',
eval Values LenTerm LenValue.
eval Values (array_intro ElemTerms) (array_intro ElemValues) :-
map (fun term value => eval Values term value) ElemTerms ElemValues.
% FIXME: This breaks for neutral terms! We should use `array_elim` here.
eval Values (array_elim ArrayTerm IndexTerm) ElemValue :-
eval Values ArrayTerm (array_intro ElemValues),
eval Values IndexTerm (int_intro Index),
list.nth ElemValues Index ElemValue.
eval Values format_type format_type.
eval Values format_intro_void format_intro_void.
eval Values format_intro_unit format_intro_unit.
eval Values format_intro_u8 format_intro_u8.
eval Values format_intro_u16le format_intro_u16le.
eval Values format_intro_u16be format_intro_u16be.
eval Values format_intro_u32le format_intro_u32le.
eval Values format_intro_u32be format_intro_u32be.
eval Values format_intro_u64le format_intro_u64le.
eval Values format_intro_u64be format_intro_u64be.
eval Values format_intro_s8 format_intro_s8.
eval Values format_intro_s16le format_intro_s16le.
eval Values format_intro_s16be format_intro_s16be.
eval Values format_intro_s32le format_intro_s32le.
eval Values format_intro_s32be format_intro_s32be.
eval Values format_intro_s64le format_intro_s64le.
eval Values format_intro_s64be format_intro_s64be.
eval Values (format_intro_array ElemType LenTerm) (format_intro_array ElemType' LenValue) :-
eval Values ElemType ElemType',
eval Values LenTerm LenValue.
eval Values (format_intro_pair FirstType SecondType) (format_intro_pair FirstType' (closure Values SecondType)) :-
eval Values FirstType FirstType'.
eval Values (format_elim Term) Value' :-
eval Values Term Value,
format_elim Value Value'.
% Closure operations
apply (closure Values Term) InputValue Value :-
eval (InputValue :: Values) Term Value.
apply_param Closure Length Value :-
apply Closure (neutral (local Length)) Value.
% Eliminations
function_elim (neutral Neutral) InputValue (neutral (function_elim Neutral InputValue)).
function_elim (function_intro Closure) InputValue OutputValue :-
apply Closure InputValue OutputValue.
pair_elim_first (neutral Neutral) (neutral (pair_elim_first Neutral)).
pair_elim_first (pair_intro FirstValue _) FirstValue.
pair_elim_second (neutral Neutral) (neutral (pair_elim_second Neutral)).
pair_elim_second (pair_intro _ SecondValue) SecondValue.
% TODO: stage_elim
% bool_elim (neutral Neutral) TrueValue FalseValue (neutral (bool_elim Neutral TrueValue FalseValue)).
% bool_elim (bool_intro true) TrueValue _ TrueValue.
% bool_elim (bool_intro false) _ FalseValue FalseValue.
% TODO: array_elim
format_elim (neutral Neutral) (neutral (format_elim Neutral)).
format_elim format_intro_void void_type.
format_elim format_intro_unit unit_type.
format_elim format_intro_u8 int_type.
format_elim format_intro_u16le int_type.
format_elim format_intro_u16be int_type.
format_elim format_intro_u32le int_type.
format_elim format_intro_u32be int_type.
format_elim format_intro_u64le int_type.
format_elim format_intro_u64be int_type.
format_elim format_intro_s8 int_type.
format_elim format_intro_s16le int_type.
format_elim format_intro_s16be int_type.
format_elim format_intro_s32le int_type.
format_elim format_intro_s32be int_type.
format_elim format_intro_s64le int_type.
format_elim format_intro_s64be int_type.
format_elim (format_intro_array Elem Len) (array_type Elem' Len) :-
format_elim Elem Elem'.
format_elim (format_intro_pair First (closure Values Term)) (pair_type First' (closure Values (format_elim Term))) :-
format_elim First First'.
% Readback of values into terms in normal form
readback : int -> neutral -> term -> prop.
readback : int -> value -> term -> prop.
% FIXME: Makam's type unification breaks hear for some reason - it
% thinks that we want to definine `int -> value -> term -> prop.`
readback Length (local Level : neutral) (local Index) :-
% Convert De Bruijn levels to De Bruijn indices using the following
% arithmetic (this is a bit awkward to express in Makam):
%
% ```
% Index = Length - (Level + 1)
% ```
plus 1 Level Level1,
plus Level1 Index Length.
readback Length (function_elim Neutral InputValue : neutral) (function_elim Term InputTerm) :-
readback Length Neutral Term,
readback Length InputValue InputTerm.
readback Length (pair_elim_first Neutral : neutral) (pair_elim_first Term) :-
readback Length Neutral Term.
readback Length (pair_elim_second Neutral : neutral) (pair_elim_second Term) :-
readback Length Neutral Term.
readback Length (format_elim Neutral : neutral) (format_elim Term) :-
readback Length Neutral Term.
readback Length (neutral Neutral) Term :-
readback Length Neutral Term.
readback Length universe universe.
readback Length void_type void_type.
readback Length unit_type unit_type.
readback Length unit_intro unit_intro.
readback Length (function_type InputType Closure) (function_type InputType' OutputType') :-
readback Length InputType InputType',
apply_param Closure Length OutputType,
plus Length 1 Length1,
readback Length1 OutputType OutputType'.
readback Length (function_intro Closure) (function_intro OutputTerm') :-
apply_param Closure Length OutputTerm,
plus Length 1 Length1,
readback Length1 OutputTerm OutputTerm'.
readback Length (pair_type FirstType Closure) (pair_type FirstType' SecondType') :-
readback Length FirstType FirstType',
apply_param Closure Length SecondType,
plus Length 1 Length1,
readback Length1 SecondType SecondType'.
readback Values (pair_intro FirstValue SecondValue) (pair_intro FirstTerm SecondTerm) :-
readback Values FirstValue FirstType,
readback Values SecondValue SecondType.
readback Length bool_type bool_type.
readback Length (bool_intro Bool) (bool_intro Bool).
readback Length int_type int_type.
readback Length (int_intro Int) (int_intro Int).
readback Length (array_type ElemValue LenValue) (array_type ElemType LenTerm) :-
readback Length ElemValue ElemType,
readback Length LenValue LenTerm.
readback Length (array_intro ElemValues) (array_intro ElemTerms) :-
map (fun value term => readback Length value term) ElemValues ElemTerms.
readback Length format_type format_type.
readback Length format_intro_void format_intro_void.
readback Length format_intro_unit format_intro_unit.
readback Length format_intro_u8 format_intro_u8.
readback Length format_intro_u16le format_intro_u16le.
readback Length format_intro_u16be format_intro_u16be.
readback Length format_intro_u32le format_intro_u32le.
readback Length format_intro_u32be format_intro_u32be.
readback Length format_intro_u64le format_intro_u64le.
readback Length format_intro_u64be format_intro_u64be.
readback Length format_intro_s8 format_intro_s8.
readback Length format_intro_s16le format_intro_s16le.
readback Length format_intro_s16be format_intro_s16be.
readback Length format_intro_s32le format_intro_s32le.
readback Length format_intro_s32be format_intro_s32be.
readback Length format_intro_s64le format_intro_s64le.
readback Length format_intro_s64be format_intro_s64be.
readback Length (format_intro_array ElemValue LenValue) (format_intro_array ElemType LenTerm) :-
readback Length ElemValue ElemType,
readback Length LenValue LenTerm.
readback Length (format_intro_pair FirstType Closure) (format_intro_pair FirstType' SecondType') :-
readback Length FirstType FirstType',
apply_param Closure Length SecondType,
plus Length 1 Length1,
readback Length1 SecondType SecondType'.
% Normalization-by-evaluation
normalize : list value -> term -> term -> prop.
normalize Values Term Term' :-
eval Values Term Value,
length Values Length,
readback Length Value Term'.
normalize : term -> term -> prop.
normalize Term Term' :-
normalize [] Term Term'.
% Equality of values
is_equal : int -> neutral -> neutral -> prop.
is_equal : int -> value -> value -> prop.
% FIXME: Makam's type unification breaks hear for some reason - it
% thinks that we want to definine `int -> value -> term -> prop.`
is_equal Length (local Level : neutral) (local Level).
is_equal Length (function_elim Neutral1 InputValue1 : neutral) (function_elim Neutral2 InputValue2) :-
is_equal Length Neutral1 Neutral2,
is_equal Length InputValue1 InputValue2.
is_equal Length (pair_elim_first Neutral1 : neutral) (pair_elim_first Neutral2) :-
is_equal Length Neutral1 Neutral2.
is_equal Length (pair_elim_second Neutral1 : neutral) (pair_elim_second Neutral2) :-
is_equal Length Neutral1 Neutral2.
is_equal Length (format_elim Neutral1 : neutral) (format_elim Neutral2) :-
is_equal Length Neutral1 Neutral2.
is_equal Length (neutral Neutral1) (neutral Neutral2) :-
is_equal Length Neutral1 Neutral2.
is_equal Length universe universe.
is_equal Length void_type void_type.
is_equal Length unit_type unit_type.
is_equal Length unit_intro unit_intro.
is_equal Length (function_type InputType1 Closure1) (function_type InputType2 Closure2) :-
is_equal Length InputType1 InputType2,
apply_param Closure1 Length OutputType1,
apply_param Closure2 Length OutputType2,
plus Length 1 Length1,
is_equal Length1 OutputType1 OutputType2.
is_equal Length (function_intro Closure1) (function_intro Closure2) :-
apply_param Closure1 Length OutputValue1,
apply_param Closure2 Length OutputValue2,
plus Length 1 Length1,
is_equal Length1 OutputValue1 OutputValue2.
is_equal Length (pair_type FirstType1 Closure1) (pair_type FirstType2 Closure2) :-
is_equal Length FirstType1 FirstType2,
apply_param Closure1 Length SecondType1,
apply_param Closure2 Length SecondType2,
plus Length 1 Length1,
is_equal Length1 SecondType1 SecondType2.
is_equal Length (pair_intro FirstTerm1 SecondTerm1) (pair_intro FirstTerm2 SecondTerm2) :-
is_equal Length FirstTerm1 FirstTerm2,
is_equal Length SecondTerm1 SecondTerm2.
is_equal Length bool_type bool_type.
is_equal Length (bool_intro Bool) (bool_intro Bool).
is_equal Length int_type int_type.
is_equal Length (int_intro Bool) (int_intro Bool).
is_equal Length (array_type ElemType1 LenTerm1) (array_type ElemType2 LenTerm2) :-
is_equal Length ElemType1 ElemType2,
is_equal Length LenTerm1 LenTerm2.
is_equal Length (array_intro ElemValues1) (array_intro ElemValues2) :-
map (fun value1 value2 => is_equal Length value1 value2) ElemValues1 ElemType2.
is_equal Length format_type format_type.
is_equal Length format_intro_void format_intro_void.
is_equal Length format_intro_unit format_intro_unit.
is_equal Length format_intro_u8 format_intro_u8.
is_equal Length format_intro_u16le format_intro_u16le.
is_equal Length format_intro_u16be format_intro_u16be.
is_equal Length format_intro_u32le format_intro_u32le.
is_equal Length format_intro_u32be format_intro_u32be.
is_equal Length format_intro_u64le format_intro_u64le.
is_equal Length format_intro_u64be format_intro_u64be.
is_equal Length format_intro_s8 format_intro_s8.
is_equal Length format_intro_s16le format_intro_s16le.
is_equal Length format_intro_s16be format_intro_s16be.
is_equal Length format_intro_s32le format_intro_s32le.
is_equal Length format_intro_s32be format_intro_s32be.
is_equal Length format_intro_s64le format_intro_s64le.
is_equal Length format_intro_s64be format_intro_s64be.
is_equal Length (format_intro_array ElemType1 LenTerm1) (format_intro_array ElemType2 LenTerm2) :-
is_equal Length ElemType1 ElemType2,
is_equal Length LenTerm1 LenTerm2.
is_equal Length (format_intro_pair FirstType1 Closure1) (format_intro_pair FirstType2 Closure2) :-
is_equal Length FirstType1 FirstType2,
apply_param Closure1 Length SecondType1,
apply_param Closure2 Length SecondType2,
plus Length 1 Length1,
is_equal Length1 SecondType1 SecondType2.
% Tests
tests : testsuite.
%testsuite tests.
% FIXME: there seems to be a bug with indenting tests here - see https://github.com/astampoulis/makam/issues/94
>> function_elim (neutral Neutral) InputValue Value ?
>> Yes:
>> Value := neutral (function_elim Neutral InputValue).
>> function_elim (function_intro (closure [] (local 0))) InputValue Value ?
>> Yes:
>> Value := InputValue.
>> pair_elim_first (neutral Neutral) Value ?
>> Yes:
>> Value := neutral (pair_elim_first Neutral).
>> pair_elim_first (pair_intro FirstValue _) Value ?
>> Yes:
>> Value := FirstValue.
>> pair_elim_second (neutral Neutral) Value ?
>> Yes:
>> Value := neutral (pair_elim_second Neutral).
>> pair_elim_second (pair_intro _ SecondValue) Value ?
>> Yes:
>> Value := SecondValue.
>> format_elim (neutral Neutral) Term ?
>> Yes:
>> Term := neutral (format_elim Neutral).
>> format_elim format_intro_u8 Term ?
>> Yes:
>> Term := int_type.
>> normalize [format_intro_u8] (local 0) Term ?
>> Yes:
>> Term := format_intro_u8.
>> normalize (ann format_intro_u8 _) Term ?
>> Yes:
>> Term := format_intro_u8.
>> normalize void_type Term ?
>> Yes:
>> Term := void_type.
>> normalize unit_type Term ?
>> Yes:
>> Term := unit_type.
>> normalize unit_intro Term ?
>> Yes:
>> Term := unit_intro.
>> normalize (function_type universe (function_type (local 0) (local 1))) Term ?
>> Yes:
>> Term := function_type universe (function_type (local 0) (local 1)).
>> normalize (function_intro (function_intro (local 0))) Term ?
>> Yes:
>> Term := function_intro (function_intro (local 0)).
>> normalize (function_elim (function_intro (local 0)) (int_intro 1)) Term ?
>> Yes:
>> Term := int_intro 1.
>> normalize (pair_type int_type (array_type int_type (local 0))) Term ?
>> Yes:
>> Term := pair_type int_type (array_type int_type (local 0)).
>> normalize (pair_elim_first (pair_intro (int_intro 0) (array_intro []))) Term ?
>> Yes:
>> Term := int_intro 0.
>> normalize (pair_elim_first (ann (pair_intro (int_intro 0) (array_intro [])) _)) Term ?
>> Yes:
>> Term := int_intro 0.
>> normalize (pair_elim_second (pair_intro (int_intro 0) (array_intro []))) Term ?
>> Yes:
>> Term := array_intro [].
>> normalize (pair_elim_second (ann (pair_intro (int_intro 0) (array_intro [])) _)) Term ?
>> Yes:
>> Term := array_intro [].
>> normalize (format_elim format_intro_u8) Term ?
>> Yes:
>> Term := int_type.
>> normalize (format_elim (format_intro_array format_intro_u8 (int_intro 3))) Term ?
>> Yes:
>> Term := array_type int_type (int_intro 3).
>> normalize (format_intro_pair format_intro_u16be (format_intro_array format_intro_u8 (local 0))) Term ?
>> Yes:
>> Term := format_intro_pair format_intro_u16be (format_intro_array format_intro_u8 (local 0)).
%end.
%extend typing.
% Bidirectional Typing
%
% This section provides an operational semantics for the declarative
% typing rules in `core.typing.declarative`, and thus is intended to be
% a _refinement_ of these rules. This means that some terms that are
% well-formed with respect to the declarative typing rules may _not_ be
% well-formed in the bidirectional typing rules, requiring additional
% type annotations in order to be considered valid.
%extend bidirectional.
% FIXME: somehow import `semantics.(value, neutral, closure)` in
% order to make this module a bit less verbose. See this comment for
% more information: https://github.com/astampoulis/makam/issues/88#issuecomment-620318340
% Bidirectional typing context.
%
% This stores the values and types of the bindings we have currently
% traversed over, allowing us to evaluate terms and synthesize the
% types of variables when we encounter them, and evaluate term.
context : type.
context : list (semantics.value * semantics.value) -> context.
%extend context.
values : context -> list semantics.value -> prop.
values (context Entries) Values :-
map tuple.fst Entries Values.
lookup_type : context -> int -> semantics.value -> prop.
lookup_type (context Entries) Index Type :-
list.nth Entries Index ( _, Type ).
next_local : context -> semantics.value -> prop.
next_local (context Entries) (semantics.neutral (semantics.local Level)) :-
length Entries Level.
add_local : context -> semantics.value -> semantics.value -> context -> prop.
add_local (context Entries) Value Type (context (( Value, Type ) :: Entries)).
add_param : context -> semantics.value -> context -> prop.
add_param Context Type Context' :-
next_local Context LocalTerm,
add_local Context LocalTerm Type Context'.
eval : context -> term -> semantics.value -> prop.
eval Context Term Value :-
values Context Values,
semantics.eval Values Term Value.
is_equal : context -> semantics.value -> semantics.value -> prop.
is_equal (context Entries) Value1 Value2 :-
length Entries Length,
semantics.is_equal Length Value1 Value2.
%end.
% Typing rules
% Check that a term is a type in the current context.
is_type : context -> term -> prop.
% Check that a term is an element of the given type in the current context.
check_type : context -> term -> semantics.value -> prop.
% Synthesize the type of a given term in the current context.
synth_type : context -> term -> semantics.value -> prop.
% A note on modes
%
% Makam does not support mode declarations (like in Mercury), but if it did
% we'd assign the following mode declarations to the above predicates:
%
% ```
% is_type : in -> in -> semidet.
% check_type : in -> in -> int -> semidet.
% synth_type : in -> in -> out -> semidet.
% ```
% Conversion
check_type Context Term Type :-
synth_type Context Term Type',
context.is_equal Context Type Type'.
% Variables
synth_type Context (local Index) Type :-
context.lookup_type Context Index Type.
% Annotated terms
% FIXME: is_type?
synth_type Context (ann Term Type) Type' :-
is_type Context Type,
context.eval Context Type Type',
check_type Context Term Type'.
% Universes
is_type Context universe.
% Unit
is_type Context unit_type.
synth_type Context unit_type semantics.universe.
synth_type Context unit_intro semantics.unit_type.
% Functions
is_type Context (function_type InputType OutputType) :-
is_type Context InputType,
context.eval Context InputType InputType',
context.add_param Context InputType' Context',
is_type Context' OutputType.
synth_type Context (function_type InputType OutputType) semantics.universe :-
is_type Context InputType,
context.eval Context InputType InputType',
context.add_param Context InputType' Context'.
is_type Context' OutputType.
check_type Context (function_intro OutputTerm) (semantics.function_type InputType Closure) :-
context.next_local Context LocalTerm,
semantics.apply Closure LocalTerm OutputType,
context.add_param Context InputType Context',
check_type Context' OutputTerm OutputType.
synth_type Context (function_elim Term InputTerm) OutputType :-
synth_type Context Term (semantics.function_type InputType Closure),
check_type Context InputTerm InputType,
context.eval Context InputTerm InputValue,
semantics.apply Closure InputValue OutputType.
% Pairs
is_type Context (pair_type FirstType SecondType) :-
check_type Context FirstType semantics.universe,
context.eval Context FirstType FirstType',
context.add_param Context FirstType' Context',
check_type Context' SecondType semantics.universe.
synth_type Context (pair_type FirstType SecondType) semantics.universe :-
check_type Context FirstType semantics.universe,
context.eval Context FirstType FirstType',
context.add_param Context FirstType' Context',
check_type Context' SecondType semantics.universe.
check_type Context (pair_intro FirstTerm SecondTerm) (semantics.pair_type FirstType Closure) :-
check_type Context FirstTerm FirstType,
context.eval Context FirstTerm FirstValue,
context.add_local Context FirstValue FirstType Context',
semantics.apply Closure FirstValue SecondType,
check_type Context' SecondTerm SecondType.
synth_type Context (pair_elim_first PairTerm) FirstType :-
synth_type Context PairTerm (semantics.pair_type FirstType _).
synth_type Context (pair_elim_second PairTerm) SecondType :-
synth_type Context PairTerm (semantics.pair_type _ Closure),
context.eval Context (pair_elim_first PairTerm) FirstValue,
semantics.apply Closure FirstValue SecondType.
% Booleans
is_type Context bool_type.
synth_type Context bool_type semantics.universe.
synth_type Context (bool_intro _) semantics.bool_type.
check_type Context (bool_elim BoolTerm TrueTerm FalseTerm) Type :-
check_type Context BoolTerm semantics.bool_type,
check_type Context TrueTerm Type,
check_type Context FalseTerm Type.
% Integers
is_type Context int_type.
synth_type Context int_type semantics.universe.
synth_type Context (int_intro _) semantics.int_type.
% Arrays
is_type Context (array_type ElemType LenTerm) :-
check_type Context ElemType semantics.universe,
check_type Context LenTerm semantics.int_type.
synth_type Context (array_type ElemType LenTerm) semantics.universe :-
check_type Context ElemType semantics.universe,
check_type Context LenTerm semantics.int_type.
check_type Context (array_intro ElemTerms) (semantics.array_type ElemType (semantics.int_intro Len)) :-
length ElemTerms Len,
map (fun elem_term => check_type Context elem_term ElemType) ElemTerms.
synth_type Context (array_elim ArrayTerm IndexTerm) ElemType :-
% FIXME: ensure `IndexTerm` is in array bounds, possibly with refinement types?
synth_type Context ArrayTerm (semantics.array_type ElemType _),
check_type Context IndexTerm semantics.int_type.
% Binary format descriptions
is_type Context format_type.
synth_type Context format_intro_unit semantics.format_type.
synth_type Context format_intro_u8 semantics.format_type.
synth_type Context format_intro_u16le semantics.format_type.
synth_type Context format_intro_u16be semantics.format_type.
synth_type Context format_intro_u32le semantics.format_type.
synth_type Context format_intro_u32be semantics.format_type.
synth_type Context format_intro_u64le semantics.format_type.
synth_type Context format_intro_u64be semantics.format_type.
synth_type Context format_intro_s8 semantics.format_type.
synth_type Context format_intro_s16le semantics.format_type.
synth_type Context format_intro_s16be semantics.format_type.
synth_type Context format_intro_s32le semantics.format_type.
synth_type Context format_intro_s32be semantics.format_type.
synth_type Context format_intro_s64le semantics.format_type.
synth_type Context format_intro_s64be semantics.format_type.
synth_type Context (format_intro_array ElemType LenTerm) semantics.format_type :-
check_type Context ElemType semantics.format_type,
check_type Context LenTerm semantics.int_type.
synth_type Context (format_intro_pair FirstType SecondType) semantics.format_type :-
check_type Context FirstType semantics.format_type,
context.eval Context (format_elim FirstType) FirstType',
context.add_param Context FirstType' Context',
check_type Context' SecondType semantics.format_type.
is_type Context (format_elim Type) :-
check_type Context Type semantics.format_type.
synth_type Context (format_elim Type) semantics.universe :-
check_type Context Type semantics.format_type.
% Convenience predicates
is_type : term -> prop.
is_type Term :-
is_type (context []) Term.
synth_type : term -> semantics.value -> prop.
synth_type Term Type :-
synth_type (context []) Term Type.
check_type : term -> semantics.value -> prop.
check_type Term Type :-
check_type (context []) Term Type.
% Tests
tests : testsuite.
%testsuite tests.
% FIXME: there seems to be a bug with indenting tests here - see https://github.com/astampoulis/makam/issues/94
>> synth_type (context [ ( semantics.format_intro_u8, semantics.format_type ) ]) (local 0) Type ?
>> Yes:
>> Type := semantics.format_type.
>> synth_type (ann format_intro_u8 format_type) Type ?
>> Yes:
>> Type := semantics.format_type.
>> check_type (ann format_intro_u8 format_type) semantics.universe ?
>> Impossible.
>> synth_type (ann int_type universe) Type ?
>> Yes:
>> Type := semantics.universe.
>> check_type (ann int_type universe) semantics.format_type ?
>> Impossible.
>> synth_type (function_type universe (function_type (local 0) (local 1))) Type ?
>> Yes:
>> Type := semantics.universe.
>> check_type (function_intro (function_intro (local 0))) (semantics.function_type semantics.universe (semantics.closure [] (function_type (local 0) (local 1)))) ?
>> Yes.
>> synth_type (function_type universe (function_type (local 0) (local 1))) Type ?
>> Yes:
>> Type := semantics.universe.
>> synth_type (function_elim (ann (function_intro (function_intro (local 0))) (function_type universe (function_type (local 0) (local 1)))) int_type) Type ?
>> Yes:
>> Type := semantics.function_type semantics.int_type (semantics.closure [ semantics.int_type ] (local 1)).
>> check_type (pair_intro (int_intro 1) (array_intro [ int_intro 42 ])) (semantics.pair_type semantics.int_type (semantics.closure [] (array_type int_type (local 0)))) ?
>> Yes.
>> synth_type (pair_elim_first (ann (pair_intro (int_intro 0) (array_intro [])) (pair_type int_type (array_type int_type (local 0))))) Type ?
>> Yes:
>> Type := semantics.int_type.
>> synth_type (pair_elim_second (ann (pair_intro (int_intro 0) (array_intro [])) (pair_type int_type (array_type int_type (local 0))))) Type ?
>> Yes:
>> Type := semantics.array_type semantics.int_type (semantics.int_intro 0).
>> check_type (array_intro []) (semantics.array_type semantics.int_type (semantics.int_intro 0)) ?
>> Yes.
>> check_type (array_intro [ int_intro 1, int_intro 2, int_intro 3 ]) (semantics.array_type semantics.int_type (semantics.int_intro 3)) ?
>> Yes.
>> check_type (format_intro_pair format_intro_u16be (format_intro_array format_intro_u8 (local 0))) semantics.format_type ?
>> Yes.
>> synth_type (format_elim (format_intro_array format_intro_u8 (int_intro 3))) Type ?
>> Yes:
>> Type := semantics.universe.
%end.
%end.
%end.
% Binary decoding/encoding
%extend binary.
byte : type.
% Decoding byte sequences into terms, guided by a format description
decode : list core.semantics.value -> list byte -> core.semantics.value -> core.semantics.value -> prop.
decode Values Bytes core.semantics.format_intro_unit core.semantics.unit_intro.
% decode Values Bytes core.semantics.format_intro_u8 (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_u16le (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_u16be (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_u32le (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_u32be (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_u64le (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_u64be (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s8 (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s16le (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s16be (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s32le (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s32be (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s64le (core.semantics.intro_int TODO).
% decode Values Bytes core.semantics.format_intro_s64be (core.semantics.intro_int TODO).
% decode Values Bytes (core.semantics.format_intro_array ElemFormat Len) TODO.
% decode Values Bytes (core.semantics.format_intro_pair FirstFormat Closure) TODO.
%end.
% Lexical syntax
%extend lexical.
token : type.
% TODO
%end.
% Surface language
%
% This language is what we expect users of the language interact with directly.
% It includes convenience features such as implicit parameters and pattern
% matching to make binary data formats easier to describe.
%extend surface.
% Surface syntax
% Terms
term : type.
%extend term.
name : string -> term.
% TODO
%end.
%end.
% Stratified language
%
% As a stepping-stone to generating Rust code (or other languages like Haskell,
% SML, or, OCaml), we first compile the core language into a language where the
% distinction between expressions, types, and kinds are made explicit.
%
% This seems to be something like [System Fω], with lifted expressions and types.
%
% We need to be careful with lifted expressions and types - this might involve
% embedding 'runtime' relevant variables being used in types, which is where
% multistage programming might ultimately help us gain more control.
%
% [System Fω]: https://en.wikipedia.org/wiki/System_F#System_F.CF.89
%extend stratified.
% Terms
kind : type.
typ : type.
expr : type.
% Variables
local : int -> typ.
local : int -> expr.
% Annotated terms
ann : typ -> kind -> typ.
ann : expr -> typ -> expr.
% 'Lifted' terms
lift : typ -> kind.
lift : expr -> typ.
% Universes
universe : kind.
% Void
void_type : typ.
% Unit
unit_type : typ.
unit_intro : expr.
% Functions
function_type : kind -> kind -> kind.
function_type : typ -> typ.
function_intro : typ -> typ.
function_intro : expr -> expr. % for terms or types
function_elim : typ -> typ -> expr.
function_elim : expr -> expr -> expr.
function_elim : expr -> typ -> expr.
% Pairs
pair_type : typ -> typ -> typ.
pair_intro : expr -> expr -> expr.
pair_elim_first : expr -> expr.
pair_elim_second : expr -> expr.
% Booleans
bool_type : typ.
bool_intro : bool -> expr.
bool_elim : expr -> expr -> expr -> expr.
% Integers
int_type : typ.
int_intro : int -> expr.
% Arrays
array_type : typ -> expr -> typ.
array_intro : list expr -> expr.
array_elim : expr -> expr -> expr.
% Binary format descriptions
format_type : kind.
format_intro_void : typ.
format_intro_unit : typ.
format_intro_u8 : typ.
format_intro_u16le : typ. % TODO: make this a computed format?
format_intro_u16be : typ. % TODO: make this a computed format?
format_intro_u32le : typ. % TODO: make this a computed format?
format_intro_u32be : typ. % TODO: make this a computed format?
format_intro_u64le : typ. % TODO: make this a computed format?
format_intro_u64be : typ. % TODO: make this a computed format?
format_intro_s8 : typ. % TODO: make this a computed format?
format_intro_s16le : typ. % TODO: make this a computed format?
format_intro_s16be : typ. % TODO: make this a computed format?
format_intro_s32le : typ. % TODO: make this a computed format?
format_intro_s32be : typ. % TODO: make this a computed format?
format_intro_s64le : typ. % TODO: make this a computed format?
format_intro_s64be : typ. % TODO: make this a computed format?
format_intro_array : typ -> expr -> typ.
format_intro_pair : typ -> typ -> typ.
format_elim : typ -> typ.
%extend semantics.
% Values
kind_value : type.
typ_value : type.
expr_value : type.
% Universes
universe : kind_value.
% Unit
unit_type : typ_value.
unit_intro : expr_value.
% Booleans
bool_type : typ_value.
bool_intro : bool -> expr_value.
% Integers
int_type : typ_value.
int_intro : int -> expr_value.
% Arrays
array_intro : list expr_value -> expr_value.
array_type : typ_value -> expr_value -> typ_value.
% Binary format descriptions
format_type : kind_value.
%end.
%end.
% Kind-erased language
%
% We take this route if our target language does not have a kind system, for
% example a language like Rust or OCaml.
%extend unkinded.
% TODO
%end.
% Uncurried language
%
% In this language functions are _uncurried_.
%extend uncurried.
% TODO
%end.
%extend rust.
typ : type.
bool : typ.
u8 : typ.
u16 : typ.
u32 : typ.
u64 : typ.
i8 : typ.
i16 : typ.
i32 : typ.
i64 : typ.
f32 : typ.
f64 : typ.
expr : type.
bool : bool -> expr.
int : int -> expr.
struct : string -> list (string * expr) -> expr.
ifte : expr -> expr -> expr -> expr.
item : type.
alias : string -> list string -> typ -> item.
struct : string -> list string -> list (string * typ) -> item.
enum : string -> list string -> list (string * typ) -> item.
function : string -> list string -> list (string * typ) -> typ -> expr -> item.
const : string -> typ -> expr -> item.
%end.
% Projections between intermediate languages.
%
% It would be fun to prototype compiling to Rust here.
%
% This course has a bunch of helpful information (in particular, Lecture 2: C
% representation): http://www.cse.chalmers.se/edu/year/2011/course/CompFun/
%
% Some challenges involve:
%
% - stratifying source terms into runtime vs compile time
% - stratifying source terms into terms and types in the target language
% - uncurrying functions
% - translating functions on types into parameterised types
% - defunctionalization/monomorphization of more complicated type functions
% - erasure of dependencies in pair types and term level functions
%extend projections.
% Bidirectional elaboration of the surface syntax into core terms
%
% Here we describe how we elaborate the surface language into the core
% language. This involves doing a number of things, including:
%
% - desugaring
% - unification
% - pattern compilation
% - etc.
%extend surface_to_core.
context : type.
% Elaboration rules
% Check that a term is a type and elaborate it to a core term.
is_type : context -> surface.term -> core.term -> prop.
% Check that a term is an element of the given type and elaborate it to a core term.
check_type : context -> surface.term -> core.semantics.value -> core.term -> prop.
% Synthesize the type of a given term and elaborate it to a core term.
synth_type : context -> surface.term -> core.semantics.value -> core.term -> prop.
% A note on modes
%
% Makam does not support mode declarations (like in Mercury), but if it did
% we'd assign the following mode declarations to the above predicates:
%
% ```
% is_type : in -> in -> out -> semidet.
% check_type : in -> in -> in -> out -> semidet.
% synth_type : in -> in -> out -> out -> semidet.
% ```
% TODO
% Conversion
% Variables
% Annotated terms
% Universes
% Void
% Unit
% Functions
% Pairs
% Booleans
% Integers
% Arrays
% Binary format descriptions
%end.
% Delaboration back into the surface language
%extend core_to_surface.
context : type.
% TODO
%end.
% Bidirectional stratification of the core language.
%extend core_to_stratified.
% Stratified terms
stratified_term : type.
kind : stratified.kind -> stratified_term.
typ : stratified.typ -> stratified_term.
expr : stratified.expr -> stratified_term.
% Stratified values
stratified_value : type.
kind : stratified.semantics.kind_value -> stratified_value.
typ : stratified.semantics.typ_value -> stratified_value.
expr : stratified.semantics.expr_value -> stratified_value.
context : type.
% Check that a term is a type and lower it to a stratified term.
is_type : context -> core.term -> stratified_term -> prop.
% Check that a term is an element of the given type and lower it to a stratified term.
check_type : context -> core.term -> stratified_value -> stratified_term -> prop.
% Synthesize the type of a given term and lower it to a stratified term.
synth_type : context -> core.term -> stratified_value -> stratified_term -> prop.
% A note on modes
%
% Makam does not support mode declarations (like in Mercury), but if it did
% we'd assign the following mode declarations to the above predicates:
%
% ```
% is_type : in -> in -> out -> semidet.
% check_type : in -> in -> in -> out -> semidet.
% synth_type : in -> in -> out -> out -> semidet.
% ```
% Conversion
% Variables
% Annotated terms
% Universes
is_type Context core.universe (kind stratified.universe).
% Void
is_type Context core.void_type (typ stratified.void_type).
synth_type Context core.void_type (kind stratified.semantics.universe) (typ stratified.void_type).
% Unit
is_type Context core.unit_type (typ stratified.unit_type).
synth_type Context core.unit_type (kind stratified.semantics.universe) (typ stratified.unit_type).
synth_type Context core.unit_intro (typ stratified.semantics.unit_type) (expr stratified.unit_intro).
% Functions
% Pairs
% Booleans
is_type Context core.bool_type (typ stratified.bool_type).
synth_type Context core.bool_type (kind stratified.semantics.universe) (typ stratified.bool_type).
synth_type Context (core.bool_intro Bool) (typ stratified.semantics.bool_type) (expr (stratified.bool_intro Bool)).
% Integers
is_type Context core.int_type (typ stratified.int_type).
synth_type Context core.int_type (kind stratified.semantics.universe) (typ stratified.int_type).
synth_type Context (core.int_intro Int) (typ stratified.semantics.int_type) (expr (stratified.int_intro Int)).
% Arrays
is_type Context (core.array_type ElemType LenTerm) (typ (stratified.array_type ElemTerm' LenTerm')) :-
check_type Context ElemType (kind stratified.semantics.universe) (typ ElemTerm'),
check_type Context LenTerm (typ stratified.semantics.int_type) (expr LenTerm').
check_type Context (core.array_type ElemType LenTerm) (kind stratified.semantics.universe) (typ (stratified.array_type ElemTerm' LenTerm')) :-
check_type Context ElemType (kind stratified.semantics.universe) (typ ElemTerm'),
check_type Context LenTerm (typ stratified.semantics.int_type) (expr LenTerm').
check_type Context (core.array_intro ElemTerms) (typ (stratified.semantics.array_type ElemType (stratified.semantics.int_intro Len))) (expr (stratified.array_intro ElemTerms')) :-
length ElemTerms Len,
map (fun elem_term elem_term' => check_type Context elem_term (typ ElemType) (expr elem_term')) ElemTerms ElemTerms'.
synth_type Context (core.array_elim ArrayTerm IndexTerm) (typ ElemType) (expr (stratified.array_elim ArrayTerm' IndexTerm')) :-
% FIXME: ensure `IndexTerm` is in array bounds, possibly with refinement types?
synth_type Context ArrayTerm (typ (stratified.semantics.array_type ElemType _)) (expr ArrayTerm'),
check_type Context IndexTerm (typ stratified.semantics.int_type) (expr IndexTerm').
% Binary format descriptions
is_type Context core.format_type (kind stratified.format_type).
synth_type Context core.format_intro_unit (kind stratified.semantics.format_type) (typ stratified.format_intro_unit).
synth_type Context core.format_intro_u8 (kind stratified.semantics.format_type) (typ stratified.format_intro_u8).
synth_type Context core.format_intro_u16le (kind stratified.semantics.format_type) (typ stratified.format_intro_u16le).
synth_type Context core.format_intro_u16be (kind stratified.semantics.format_type) (typ stratified.format_intro_u16be).
synth_type Context core.format_intro_u32le (kind stratified.semantics.format_type) (typ stratified.format_intro_u32le).
synth_type Context core.format_intro_u32be (kind stratified.semantics.format_type) (typ stratified.format_intro_u32be).
synth_type Context core.format_intro_u64le (kind stratified.semantics.format_type) (typ stratified.format_intro_u64le).
synth_type Context core.format_intro_u64be (kind stratified.semantics.format_type) (typ stratified.format_intro_u64be).
synth_type Context core.format_intro_s8 (kind stratified.semantics.format_type) (typ stratified.format_intro_s8).
synth_type Context core.format_intro_s16le (kind stratified.semantics.format_type) (typ stratified.format_intro_s16le).
synth_type Context core.format_intro_s16be (kind stratified.semantics.format_type) (typ stratified.format_intro_s16be).
synth_type Context core.format_intro_s32le (kind stratified.semantics.format_type) (typ stratified.format_intro_s32le).
synth_type Context core.format_intro_s32be (kind stratified.semantics.format_type) (typ stratified.format_intro_s32be).
synth_type Context core.format_intro_s64le (kind stratified.semantics.format_type) (typ stratified.format_intro_s64le).
synth_type Context core.format_intro_s64be (kind stratified.semantics.format_type) (typ stratified.format_intro_s64be).
% TODO: core.format_intro_array
% TODO: core.format_intro_pair
% TODO: core.format_elim
%end.
% Erasure of kinds
%extend stratified_to_unkinded.
% TODO
%end.
%extend unkinded_to_uncurried.
% TODO
%end.
%extend uncurried_to_rust.
% TODO
%end.
%end.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment