lol-calculus: Calculus for LOL (λω language).

[ gpl, language ] [ Propose Tags ]

WARNING: this is a research program written as I learn and explore lambda calculii: please understand well by yourself whatever you may take from it; any question or contribution being welcome :-)

This package implements an explicitely typed (aka. à la Church) lambda calculus with: simples types, parametric polymorphism, higher-rank polymorphism and constructors of types (I have no need for dependent types so far, but it should be straightforward to add them to allow the full Calculus of constructions (CoC)).

This is mainly done by means of: a common Algebraic Data Type (ADT) for terms and types to build a Pure Type System (PTS), generalized DeBruijn indices to implement capture-avoiding substitution of variables, and Typeable axioms to embed Haskell types and terms (the most experimental and tricky part).

The inspiring programs I studied which explore similar problems: Simon Peyton Jones and Erik Meijer's Henk, Dan Doel's pts, Gabriel Gonzalez's morte, Richard Eisenberg's glambda, Edward Kmett's bound.

See also: the lol-typing package studying the type inferencing.

NOTE: if you are just interested in building an Embedded Domain Specific Language (EDSL) you may as well study Oleg Kiselyov, Jacques Carette and Chung-chieh Shan's Typed Tagless Final Interpreters, which you may find being a much more simple, efficient and robust approach.

Modules

  • Language
    • LOL
      • Language.LOL.Calculus
        • Language.LOL.Calculus.Abstraction
        • Language.LOL.Calculus.Axiom
        • Language.LOL.Calculus.Form
        • Language.LOL.Calculus.Read
        • Language.LOL.Calculus.Term
        • Language.LOL.Calculus.Type

Flags

Manual Flags

NameDescriptionDefault
dev

Turn on development settings.

Disabled
dump

Dump some intermediate files.

Disabled
prof

Turn on profiling settings.

Disabled
threaded

Enable threads.

Disabled
Automatic Flags
NameDescriptionDefault
exe

Build executable.

Enabled
lib

Build library.

Enabled

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

Versions [RSS] 1.20160822
Dependencies base (>=4.6 && <5), containers (>=0.5 && <0.6), directory, filepath, haskeline (>=0.7 && <0.8), lol-calculus, mtl (>=2.0), parsec (>=3.1.2 && <4), text, text-format, transformers (>=0.4 && <0.5) [details]
License GPL-3.0-only
Author Julien Moutinho <julm+lol@autogeree.net>
Maintainer Julien Moutinho <julm+lol@autogeree.net>
Category Language
Source repo head: git clone git://git.autogeree.net/lol
Uploaded by julm at 2016-08-23T05:14:54Z
Distributions NixOS:1.20160822
Reverse Dependencies 1 direct, 1 indirect [details]
Executables lol-calculus
Downloads 707 total (3 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-11-20 [all 1 reports]