Popularity
7.3
Growing
Activity
5.1
-
22
5
3

Monthly Downloads: 14
Programming language: Haskell
License: MIT License

helf alternatives and similar packages

Based on the "Dependent Types" category.
Alternatively, view helf alternatives based on common mentions on social networks and blogs.

Do you think we are missing an alternative of helf or a related project?

Add another 'Dependent Types' Package

README

helf

A Haskell implementation of the Edinburgh Logical Framework.

helf parses and typechecks .elf files written for the Twelf implementation of the Logical Framework. helf is mainly a laboratory to experiment with different representation of lambda-terms for bidirectional typechecking.

Limitations

helf only understands a subset of the Twelf language and implements only a small subset of Twelf's features.

  • helf does not parse the backarrow <- notation for function space.
  • helf only understands the fixity pragmas for operators. It ignores all other pragmas.
  • helf only implements bidirectional type checking. It does not have unification or type reconstruction.
  • helf does not give nice error messages.

Installation

Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type

  cabal install helf

Examples

File eval.elf:

% Untyped lambda calculus.

tm   : type.
abs  : (tm -> tm) -> tm.
app  : tm -> (tm -> tm).

% cbn weak head evaluation.

eval : tm -> tm -> type.

eval/abs : {M : tm -> tm}
  eval (abs M) (abs M).

eval/app : {M : tm} {M' : tm -> tm} {N : tm} {V : tm}
  eval M (abs M') ->
  eval (M' N) V   ->
  eval (app M N) V.

Type check with:

  helf eval.elf

For more examples, see test/succeed/.