Delta-Lambda: A demonstration interpreter for type system delta-lambda (of N.G. De-bruijn)

[ compilers-interpreters, mit, program ] [ Propose Tags ]

A demonstration package for the type system delta-lambda (of N.G. De-bruijn) in ~1000 lines of haskell. this is at the moment exceptionally ALPHA level software. no tests for the validity of the type checker (only the type synthesizer), or the parser, or the repl, etc... there are dragons in here (soon to be tamed), and lots of them! todo: profiling, unit testing, formal verification of type correctness adequacy proof of the implemented type system.


[Skip to Readme]

Flags

Manual Flags

NameDescriptionDefault
debug

Enable debugging

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.2.0.0, 0.3.0.0
Dependencies base (>=4.8 && <4.10), bytestring (>=0.10.6.0), Cabal (>=1.9.2), cereal (>=0.5 && <0.6), cpphs (>=1.20), filepath (>=1.4.0.0), haskeline (>=0.7 && <0.8), megaparsec (>=5.0 && <5.3), mtl (>=2.2 && <2.3), options (>=1.2 && <1.3), parallel (>=3.2 && <3.3), text (>=1.2.2.0), wl-pprint (>=1.2) [details]
License MIT
Copyright Copyright (c) 2016 James M Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
Author James M
Maintainer listofoptions@gmail.com
Category Compilers/Interpreters
Home page https://github.com/listofoptions/delta-lambda
Bug tracker https://github.com/listofoptions/delta-lambda/issues
Source repo head: git clone git://github.com/listofoptions/delta-lambda.git
Uploaded by listofoptions at 2017-05-11T01:32:18Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Executables Delta-Lambda
Downloads 2678 total (6 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2017-05-11 [all 3 reports]

Readme for Delta-Lambda-0.3.0.0

[back to package description]

ΔΛ (Delta-Lambda)

Build Status

Introduction :

This language is a test language for an implementation of the type system ΔΛ (Delta-Lambda) described by de Bruijn for simplifying the semantics of his Automath project. Eventually I will post the Coq/Idris/Agda/etc... proofs for the compliance of the code to the inferential rules specified by De Groote.

Syntax :

The syntax is expressed in EBNF.

expression syntax

Expression  = 'type'
	          | Identifier
            | '(' , Expression  , { ',' , Expression  } , ')' , Expression
            | '[' , Declaration , { ',' , Declaration } , ']' , Expression
            ;
Declaration = [ Identifier , { ',' , Identifier } ] ':' Expression
            ;

Semantics :

the semantics of delta-lambda are fairly simple, and involve inductive definitions on the structure of expressions. We will step through the inductive relations on terms and describe them in detail. We assume that beta equivalence is known to be the reflexive transitive symmetric closure of beta reduction, which is defined as normal. the notation [x := A]B is used to represent substitution, which also takes on the typical meaning (pedants may examine de Bruijn's paper)

here are the relations (the names of which are the same in the code):

  1. typeOf
  • the typeOf function produces the type of a term, by replacing the tail variable with it's type

typeOf[context, x] = A if [x : A] in context

typeOf[context, (A) B] = (A) typeOf[context, B]

typeOf[context, [x : A] B] = [x: A] typeOf[[x : A] context, B])

  1. ftype
  • this function produces the 'final' type of a term, that is the term ends in type. (note that this essentially preforms eta expansion)

ftype[context, A] = A if tail[A] is type

ftype[context, A] = typef[context, typeOf[context, A]] if tail[A] is not type

  1. tail
  • this function computes the term at the 'end' of a spine.

tail[type] = type

tail[x] = x

tail[(A) B] = tail[B]

tail[[x : A] B] = tail[B]

  1. correct
  • this is the most important structural function, it's purpose is to prove (or disprove) that a given term is (or is not) correct.

correct[context, type] = true

correct[context, x] = true iff (x A) in context, else false

correct[context, [x : A] B] = correct[context, A] and correct[[x : A] context, B]

correct[context, (A) B] = correct[B] and typing[context, A] is beta equivalent to some [x : C] D and typeOf[context, B] is beta equivalent to C and correct[context, [x := B]D]

It must be reiterated that proofs of the conformance of these structural relations on Expressions have not been written yet, as the relations are not simply recursive, so a proof in Coq/Agda/Idris/etc... will be very difficult Also note that the code does not exactly follow this formalism.

References :