symantic: Library for Typed Tagless-Final Higher-Order Composable DSL
This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting a custom DSL (Domain-Specific Language) expressing a subset of GHC's Haskell type system:
first class functions (aka. lambdas),
chosen monomorphic types (like
chosen rank-1 polymorphic types (like
chosen type class instances,
chosen type family instances,
and chosen type constraints;
where "chosen X" means declared in Haskell and selected when composing the DSL.
In particular, this library is currently not able to:
do type inferencing for the argument of lambdas (they must all be explicitely annotated, aka. Church-style),
do pattern matching (aka. case) (but Church-encoding functions are often enough),
do rank-N polymorphic types (aka. non-prenex forall, like
(forall s. ST s a) -> a).
And by itself, the DSL is only able to define new terms to be interpreted, no new types, or other type-level structures.
Please be aware that despite its using of powerful ideas from clever people, this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY. Meaning that it IS NOT heavily tested and documented, DOES NOT have a strong commitment to preserving backward compatibility, MAY FAIL to comply with the PVP, and CAN die without notice. You've been warned.
The main goal of this library is to enable the runtime interpretation of terms, type-checked according to some types defined at composing-time (ie. GHC's compile-time).
Using a DSL enables to limit expressiveness in order to ease analysis. Here the idea is that the more complex logic shall remain written in Haskell, and then this library used to project an interface into a DSL (using GHC's Haskell as a FFI (Foreign Function Interface)). This in order to give runtime users the flexibility to write programs not requiring a full-blown Haskell compiler, yet enabling enough flexibility to let them express complex needs with a reasonably advanced type-safe way and a controlled environment of primitives.
Typical use cases:
Enabling runtime users to enter some Haskell-like expressions (maybe with a more convenient syntax wrt. the domain problem) without using at runtime all the heavy machinery and ecosystem of GHC (eg. by using hint), but still leaning on primitive functions coded in GHC's Haskell.
Limiting those expressions to be built from well-controlled expressions only.
Run some analyzes/optimizations on those well-controlled expressions.
Please pick in symantic-lib
a few specific
Lib/*.hs files near what you want to do
and the corresponding
if any in the Git repository,
to learn by examples how to use this library.
Lib/*/Test.hs files use megaparsec as parser
Grammar/Megaparsec.hs) and a default grammar somehow sticking to Haskell's,
but staying context-free (so in particular: insensitive to the indentation),
and supporting prefix and postfix operators.
This grammar — itself written as a symantic embedded DSL
with symantic-grammar —
can be reused to build other ones, is not bound to a specific parser,
and can produce its own EBNF rendition.
This library would probably be much worse than it is without the following seminal works:
Finally Tagless by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
Dependent Types in Haskell by Richard A. Eisenberg.
Symantic DSL. Terms are encoded in the Tagless-Final way (aka. the symantic way) which leverages the type class system of Haskell — instead of using data types — to form an embedded DSL. More specifically, a class encodes the syntax of terms (eg.
Sym_Bool) and its class instances on a dedicated type encodes their semantics (eg.
(Sym_Bool Eval)interprets a term as a value of its type in the host language (
Boolin Haskell here), or
(Sym_Bool View)interprets a term as a textual rendition, etc.). DSL are then composedextended by selecting those symantic classes/ (and in an embedded DSL those could even be automatically inferred, when
NoMonomorphismRestrictionis on). Otherwise, when using symantics for a non-embedded DSL — the whole point of this library — the classes composing the DSL are selected manually at GHC's compile-time, through the type-level list
readTerm. Moreover, those symantic
terms are parameterized by the type of the value they encode, in order to get the same type safety as with plain Haskell values. Hence the symantic classes have the higher kind:
((* -> *) -> Constraint)instead of just
(* -> Constraint). Amongst those symantics,
Sym_Lambdaintroduces lambda abstractions by an higher-order approach, meaning that they directly reuse GHC's internal machinery to abstract or instantiate variables, which I think is by far the most efficient and simplest way of doing it (no (generalized or not) DeBruijn encoding like in bound's
Singleton for any type. To typecheck terms using a
src vs t)which acts as a singleton type for any Haskell type index
tof any kind, which is made possible with the dependant Haskell extensions: especially
Type constants using
Typeable. Type constant could be introduced by indexing them amongst a type-level list, but since they are monomorphic types, using
Typeablesimplifies the machinery, and is likely more space/time efficient, including at GHC-compile-time.
Type variables using a type-level list. Handling type variables is done by indexing them amongst a
vstype-level list, where each type variable is wrapped inside a
Proxyto handle different kinds. Performing a substitution (in
substVar) preserves the type index
t, which is key for preserving any associated
Term. Unifying type variables is done with
unifyType), which I think is necessary and likely safe.
AllowAmbiguousTypesfor avoiding a lot of uses of
ConstraintKindsfor type lists to contain
Constraints, or reifying any
Constraintas an explicit dictionary
Dict, or defining type synonym of type classes, or merging type constraints.
DataKindsfor type-level data structures (eg. type-level lists).
DefaultSignaturesfor providing identity transformations of terms, and thus avoid boilerplate code when a transformation does not need to alter all semantics. Almost as explained in Reducing boilerplate in finally tagless style.
GADTsfor knowing types by pattern-matching terms, or building terms by using type classes.
PolyKindsfor avoiding a lot of uses of
TypeApplicationsfor having a more concise syntax to build
TypeFamiliesfor type-level programming.
TypeInType(introduced in GHC 8.0.1) for
Typeto also bind a kind equality for the type
tit encodes. Which makes the type application (
TyApp) give us an arrow kind for the Haskell type constructor it applies an Haskell type to, releaving me from tricky workarounds.
UndecidableInstancesfor type-level programming that may never terminate.
There are some of them hidding in there, and the whole thing is far from being perfect… Your comments, problem reports, or questions, are welcome! You have my email address, so… just send me some emails :]
Study to which point type inferencing is doable, now that
Typeis powerful enough to contain
Study to which point error messages can be improved, now that there is a
Sourcecarried through all
Types, it should enable some nice reports. Still, a lot of work and testing remain to be done, and likely some ideas to find too…
Add more terms in symantic-lib.
Add more transformations.
Study how to integrate types into the module system.
Study where to put
Study how to support rank-N polymorphic types, special cases can likely use the boxed polymorphism workaround, but even if GHC were supporting impredicative types, I'm currently clueless about how to do this.
|Versions [faq]||126.96.36.19970623, 188.8.131.5270702, 184.108.40.20670703, 220.127.116.1170807, 18.104.22.16880213, 22.214.171.12480208, 126.96.36.19990614, 188.8.131.5290712|
|Dependencies||base (>=4.6 && <5), containers, ghc-prim, mono-traversable, symantic-document, symantic-grammar, text, transformers [details]|
|Author||Julien Moutinho <email@example.com>|
|Maintainer||Julien Moutinho <firstname.lastname@example.org>|
|Bug tracker||Julien Moutinho <email@example.com>|
|Source repo||head: git clone git://git.autogeree.net/symantic|
|Uploaded||by julm at 2017-06-23T18:05:14Z|
|Downloads||3638 total (8 in the last 30 days)|
|Rating||(no votes yet) [estimated by Bayesian average]|
Docs available [build log]
Last success reported on 2017-06-23 [all 1 reports]
For package maintainers and hackage trustees