--- /dev/null
+# symantic
+
+This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting
+a custom DSL (Domain-Specific Language).
+
+# Features
+
+Those custom DSL can express a subset of GHC's Haskell type system:
+
+* *first class functions* (aka. *lambdas*),
+* chosen *monomorphic types* (like `Bool` or `Maybe`),
+* chosen *rank-1 polymorphic types* (like `(Maybe a)`),
+* 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.
+
+# Warning
+
+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](http://www.haskell.org/haskellwiki/Package_versioning_policy),
+and CAN die without notice.
+You've been warned.
+
+# Use cases
+
+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](https://hackage.haskell.org/package/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.
+* Report errors specific to the domain problem.
+
+# Usage
+
+Please pick in [symantic-lib](https://hackage.haskell.org/package/symantic-lib)
+a few specific `Lib/*.hs` files near what you want to do
+and the corresponding `Lib/*/Test.hs` file,
+if any in the [Git repository](git://git.autogeree.net/symantic),
+to learn by examples how to use this library.
+
+Those `Lib/*/Test.hs` files use [megaparsec](https://hackage.haskell.org/package/megaparsec) as parser
+(see `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](https://hackage.haskell.org/package/symantic-grammar) —
+can be reused to build other ones, is not bound to a specific parser,
+and can produce its own EBNF rendition.
+
+# Acknowledgements
+
+This library would probably be much worse than it is
+without the following seminal works:
+
+* [Finally Tagless](http://okmij.org/ftp/tagless-final/) by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
+* [Dependent Types in Haskell](http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) by Richard A. Eisenberg.
+
+# Main ideas
+
+* __Symantic DSL__.
+ Terms are encoded in the [Tagless-Final](http://okmij.org/ftp/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 (`Bool` in Haskell here),
+ or `(Sym_Bool View)` interprets a term as a textual rendition, etc.).
+
+ DSL are then composed/extended by selecting those symantic *classes*
+ (and in an embedded DSL those could even be automatically inferred,
+ when `NoMonomorphismRestriction` is 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* `ss` given to `readTerm`.
+
+ Moreover, those symantic `term`s 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_Lambda` introduces *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](https://hackage.haskell.org/package/bound)'s `Monad`s).
+
+* __Singleton for any type__.
+ To typecheck terms using a `(Type src vs t)` which acts as a *singleton type*
+ for any Haskell *type index* `t` of any kind,
+ which is made possible with the dependant Haskell extensions:
+ especially `TypeFamilies`, `GADTs` and `TypeInType`.
+
+* __Type constants using `Typeable`__.
+ *Type constant* could be introduced by indexing them amongst a *type-level list*,
+ but since they are *monomorphic types*, using `Typeable` simplifies
+ 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 `vs` *type-level list*,
+ where each *type variable* is wrapped inside a `Proxy` to 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 `unsafeCoerce` (in `unifyType`),
+ which I think is necessary and likely safe.
+
+# Main extensions
+
+* `AllowAmbiguousTypes` for avoiding a lot of uses of `Proxy`.
+* `ConstraintKinds` for *type lists* to contain `Constraint`s,
+ or reifying any `Constraint` as an explicit dictionary `Dict`,
+ or defining *type synonym* of *type classes*,
+ or merging *type constraints*.
+* `DataKinds` for type-level data structures (eg. *type-level lists*).
+* `DefaultSignatures` for 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](https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate).
+* `GADTs` for knowing types by pattern-matching terms,
+ or building terms by using type classes.
+* `PolyKinds` for avoiding a lot of uses of `Proxy`.
+* `Rank2Types` or `ExistentialQuantification` for parsing `GADT`s.
+* `TypeApplications` for having a more concise syntax
+ to build `Type` (eg. `tyConst `Bool`).
+* `TypeFamilies` for type-level programming.
+* `TypeInType` (introduced in GHC 8.0.1)
+ for `Type` to also bind a kind equality for the type `t` it 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.
+* `UndecidableInstances` to relax the checks that the type-level programming does terminate.
+
+# Bugs
+
+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 :]
+
+# To do
+
+* Study to which point *type inferencing* is doable,
+ now that `Type` is powerful enough to contain `TyVar`s.
+* Study to which point error messages can be improved,
+ now that there is a `Source` carried through all `Kind`s or `Type`s,
+ 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](https://hackage.haskell.org/package/symantic-lib).
+* Add more transformations.
+* Study how to list class instances.
+* Study where to put `INLINE`, `INLINEABLE` or `SPECIALIZE` pragmas.
+* 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.
build-type: Simple
cabal-version: >= 1.24
category: Language
-description:
- __Description__
- .
- 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 'Bool' or 'Maybe'),
- * chosen /rank-1 polymorphic types/ (like @(@'Maybe'@ a)@),
- * 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.
- .
- __Warning__
- .
- 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 <http://www.haskell.org/haskellwiki/Package_versioning_policy PVP>,
- and CAN die without notice.
- You've been warned.
- .
- __Use cases__
- .
- 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 <https://hackage.haskell.org/package/hint 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.
- * Report errors specific to the domain problem.
- .
- __Usage__
- .
- Please pick in <https://hackage.haskell.org/package/symantic-lib symantic-lib>
- a few specific @Lib/*.hs@ files near what you want to do
- and the corresponding @Lib\/*/Test.hs@ file,
- if any in the <git://git.autogeree.net/symantic Git repository>,
- to learn by examples how to use this library.
- .
- Those @Lib\/*/Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser
- (see @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 <https://hackage.haskell.org/package/symantic-grammar symantic-grammar> —
- can be reused to build other ones, is not bound to a specific parser,
- and can produce its own EBNF rendition.
- .
- __Acknowledgements__
- .
- This library would probably be much worse than it is
- without the following seminal works:
- .
- * <http://okmij.org/ftp/tagless-final/ Finally Tagless> by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
- * <http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf Dependent Types in Haskell> by Richard A. Eisenberg.
- .
- __Main ideas__
- .
- * __Symantic DSL__.
- Terms are encoded in the <http://okmij.org/ftp/tagless-final/ 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 ('Bool' in Haskell here),
- or @(Sym_Bool View)@ interprets a term as a textual rendition, etc.).
-
- DSL are then composed\/extended by selecting those symantic /classes/
- (and in an embedded DSL those could even be automatically inferred,
- when @NoMonomorphismRestriction@ is 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/ @ss@ given to 'readTerm'.
-
- Moreover, those symantic @term@s 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_Lambda' introduces /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 <https://hackage.haskell.org/package/bound bound>'s @Monad@s).
-
- * __Singleton for any type__.
- To typecheck terms using a @(@'Type'@ src vs t)@ which acts as a /singleton type/
- for any Haskell /type index/ @t@ of any kind,
- which is made possible with the dependant Haskell extensions:
- especially @TypeFamilies@, @GADTs@ and @TypeInType@.
-
- * __Type constants using 'Typeable'__.
- /Type constant/ could be introduced by indexing them amongst a /type-level list/,
- but since they are /monomorphic types/, using 'Typeable' simplifies
- 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 @vs@ /type-level list/,
- where each /type variable/ is wrapped inside a @Proxy@ to 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 'unsafeCoerce' (in 'unifyType'),
- which I think is necessary and likely safe.
-
- -- NOTE: no longer used.
- -- * __Extensible data type__.
- -- To inject a type into a /type-level list/
- -- or project a /type-level list/ onto a type,
- -- to compose an /extensible data type/
- -- (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,
- -- that a parser can build and then give to 'compile').
- -- This type-level programming requires @UndecidableInstances@,
- -- but not @OverlappingInstances@.
- --
- -- There is a similarity with
- -- <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>
- -- (see for instance <https://hackage.haskell.org/package/compdata compdata>
- -- or <https://hackage.haskell.org/package/syntactic syntactic>).
- -- Those also enable to compose a DSL using some machinery
- -- based upon (co)free(r) (co)monads and (cata|ana)morphisms.
- -- Which library fits best your problem domain and brain is for you to judge :)
- -- On that topic, see also:
- -- <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.
- --
- -- Here, I just came up using /type-level lists/ by hacking
- -- <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.
- .
- __Main extensions__
- .
- * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'.
- * @ConstraintKinds@ for /type lists/ to contain 'Constraint's,
- or reifying any 'Constraint' as an explicit dictionary 'Dict',
- or defining /type synonym/ of /type classes/,
- or merging /type constraints/.
- * @DataKinds@ for type-level data structures (eg. /type-level lists/).
- * @DefaultSignatures@ for providing identity transformations of terms,
- and thus avoid boilerplate code when a transformation
- does not need to alter all semantics.
- Almost as explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.
- * @GADTs@ for knowing types by pattern-matching terms,
- or building terms by using type classes.
- * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.
- * @Rank2Types@ or @ExistentialQuantification@ for parsing @GADT@s.
- * @TypeApplications@ for having a more concise syntax
- to build 'Type' (eg. 'tyConst'@ @\@Bool).
- * @TypeFamilies@ for type-level programming.
- * @TypeInType@ (introduced in GHC 8.0.1)
- for 'Type' to also bind a kind equality for the type @t@ it 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.
- * @UndecidableInstances@ to relax the checks that the type-level programming does terminate.
- .
- __Bugs__
- .
- 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 :]
- .
- __To do__
- .
- * Study to which point /type inferencing/ is doable,
- now that 'Type' is powerful enough to contain 'TyVar's.
- * Study to which point error messages can be improved,
- now that there is a 'Source' carried through all 'Kind's or 'Type's,
- 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 <https://hackage.haskell.org/package/symantic-lib symantic-lib>.
- * Add more transformations.
- * Study how to integrate types into the module system.
- * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.
- * 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.
+description: 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.
extra-source-files:
extra-tmp-files:
-- homepage:
Language.Symantic.Typing.Grammar
Language.Symantic.Typing.Kind
Language.Symantic.Typing.List
+ Language.Symantic.Typing.Module
Language.Symantic.Typing.Peano
Language.Symantic.Typing.Read
Language.Symantic.Typing.Show
sourcephile / git / haskell / symantic.git / commitdiff