lol-calculus: Calculus for LOL (λω language).
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
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.
Properties
| Versions | 1.20160822, 1.20160822 |
|---|---|
| Change log | None available |
| 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:05:09Z |
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
- Language.LOL.Calculus
- LOL
Flags
Manual Flags
| Name | Description | Default |
|---|---|---|
| dev | Turn on development settings. | Disabled |
| dump | Dump some intermediate files. | Disabled |
| prof | Turn on profiling settings. | Disabled |
| threaded | Enable threads. | Disabled |
Automatic Flags
| Name | Description | Default |
|---|---|---|
| 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
- lol-calculus-1.20160822.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees