symantic/README.md

   1 # symantic
   2
   3 This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting
   4 a custom DSL (Domain-Specific Language).
   5
   6 # Features
   7
   8 Those custom DSL can express a subset of GHC's Haskell type system:
   9
  10 * *first class functions* (aka. *lambdas*),
  11 * chosen *monomorphic types* (like `Bool` or `Maybe`),
  12 * chosen *rank-1 polymorphic types* (like `(Maybe a)`),
  13 * chosen *type class instances*,
  14 * chosen *type family instances*,
  15 * and chosen *type constraints*;
  16
  17 where "chosen X" means declared in Haskell
  18 and selected when composing the DSL.
  19
  20 In particular, this library is currently not able to:
  21
  22 * do *type inferencing* for the argument of *lambdas*
  23   (they must all be explicitely annotated, aka. *Church-style*),
  24 * do *pattern matching* (aka. *case*) (but *Church-encoding* functions are often enough),
  25 * do *rank-N polymorphic types* (aka. *non-prenex forall*, like `(forall s. ST s a) -> a`).
  26
  27 And by itself, the DSL is only able to define new terms to be interpreted,
  28 no new types, or other type-level structures.
  29
  30 # Warning
  31
  32 Please be aware that despite its using of powerful ideas from clever people,
  33 this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY.
  34 Meaning that it IS NOT heavily tested and documented,
  35 DOES NOT have a strong commitment to preserving backward compatibility,
  36 MAY FAIL to comply with the [PVP](http://www.haskell.org/haskellwiki/Package_versioning_policy),
  37 and CAN die without notice.
  38 You've been warned.
  39
  40 # Use cases
  41
  42 The main goal of this library is to enable the runtime interpretation of terms,
  43 type-checked according to some types defined at composing-time (ie. GHC's compile-time).
  44
  45 Using a DSL enables to limit expressiveness in order to ease analysis.
  46 Here the idea is that the more complex logic shall remain written in Haskell,
  47 and then this library used to project an interface into a DSL
  48 (using GHC's Haskell as a FFI (Foreign Function Interface)).
  49 This in order to give runtime users the flexibility
  50 to write programs not requiring a full-blown Haskell compiler,
  51 yet enabling enough flexibility to let them express complex needs
  52 with a reasonably advanced type-safe way
  53 and a controlled environment of primitives.
  54
  55 ## Typical use cases
  56
  57 * Enabling runtime users to enter some Haskell-like expressions
  58   (maybe with a more convenient syntax wrt. the domain problem)
  59   without using at runtime all the heavy machinery and ecosystem of GHC
  60   (eg. by using [hint](https://hackage.haskell.org/package/hint)),
  61   but still leaning on primitive functions coded in GHC's Haskell.
  62 * Limiting those expressions to be built from well-controlled expressions only.
  63 * Run some analyzes/optimizations on those well-controlled expressions.
  64 * Report errors specific to the domain problem.
  65
  66 # Usage
  67
  68 Please pick in [symantic-lib](https://hackage.haskell.org/package/symantic-lib)
  69 a few specific `Lib/*.hs` files near what you want to do
  70 and the corresponding `Lib/*/Test.hs` file,
  71 if any in the [Git repository](git://git.autogeree.net/symantic),
  72 to learn by examples how to use this library.
  73
  74 Those `Lib/*/Test.hs` files use [megaparsec](https://hackage.haskell.org/package/megaparsec) as parser
  75 (see `Grammar/Megaparsec.hs`) and a default grammar somehow sticking to Haskell's,
  76 but staying context-free (so in particular: insensitive to the indentation),
  77 and supporting prefix and postfix operators.
  78 This grammar — itself written as a symantic embedded DSL
  79 with [symantic-grammar](https://hackage.haskell.org/package/symantic-grammar) —
  80 can be reused to build other ones, is not bound to a specific parser,
  81 and can produce its own EBNF rendition.
  82
  83 # Acknowledgements
  84
  85 This library would probably be much worse than it is
  86 without the following seminal works:
  87
  88 * [Finally Tagless](http://okmij.org/ftp/tagless-final/) by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
  89 * [Dependent Types in Haskell](http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf) by Richard A. Eisenberg.
  90 * [A reflection on types](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/dynamic.pdf) by Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg and Dimitrios Vytiniotis.
  91 * [Typeable](https://ghc.haskell.org/trac/ghc/wiki/Typeable) by Ben Gamari and others.
  92
  93 # Main ideas
  94
  95 * __Symantic DSL__.
  96   Terms are encoded in the [Tagless-Final](http://okmij.org/ftp/tagless-final/) way (aka. the *symantic* way)
  97   which leverages the *type class* system of Haskell — instead of using *data types* — to form an embedded DSL.
  98   More specifically, a *class* encodes the *syntax* of terms (eg. `Sym_Bool`)
  99   and its *class instances* on a dedicated type encodes their *semantics*
 100   (eg. `(Sym_Bool Eval)` interprets a term as a value of its type
 101   in the host language (`Bool` in Haskell here),
 102   or `(Sym_Bool View)` interprets a term as a textual rendition, etc.).
 103
 104   DSL are then composed/extended by selecting those symantic *classes*
 105   (and in an embedded DSL those could even be automatically inferred,
 106   when `NoMonomorphismRestriction` is on).
 107   Otherwise, when using symantics for a non-embedded DSL
 108   — the whole point of this library — the *classes* composing the DSL
 109   are selected manually at GHC's compile-time,
 110   through the *type-level list* `ss` given to `readTerm`.
 111
 112   Moreover, those symantic `term`s are parameterized by the type of the value they encode,
 113   in order to get the same type safety as with plain Haskell values.
 114   Hence the symantic *classes* have the higher kind: `((* -> *) -> Constraint)`
 115   instead of just `(* -> Constraint)`.
 116
 117   Amongst those symantics, `Sym_Lambda` introduces *lambda abstractions* by an higher-order approach,
 118   meaning that they directly reuse GHC's internal machinery
 119   to abstract or instantiate variables,
 120   which I think is by far the most efficient and simplest way of doing it
 121   (no (generalized or not) DeBruijn encoding
 122   like in [bound](https://hackage.haskell.org/package/bound)'s `Monad`s).
 123
 124 * __Singleton for any type__.
 125   To typecheck terms using a `(Type src vs t)` which acts as a *singleton type*
 126   for any Haskell *type index* `t` of any kind,
 127   which is made possible with the dependant Haskell extensions:
 128   especially `TypeFamilies`, `GADTs` and `TypeInType`.
 129
 130 * __Type constants using `Typeable`__.
 131   *Type constant* could be introduced by indexing them amongst a *type-level list*,
 132   but since they are *monomorphic types*, using `Typeable` simplifies
 133   the machinery, and is likely more space/time efficient, including at GHC-compile-time.
 134
 135 * __Type variables using a type-level list__.
 136   Handling *type variables* is done by indexing them amongst a `vs` *type-level list*,
 137   where each *type variable* is wrapped inside a `Proxy` to handle different kinds.
 138   Performing a substitution (in `substVar`) preserves the *type index* `t`,
 139   which is key for preserving any associated `Term`.
 140   Unifying *type variables* is done with `unsafeCoerce` (in `unifyType`),
 141   which I think is necessary and likely safe.
 142
 143 # Main extensions
 144
 145 * `AllowAmbiguousTypes` for avoiding a lot of uses of `Proxy`.
 146 * `ConstraintKinds` for *type lists* to contain `Constraint`s,
 147   or reifying any `Constraint` as an explicit dictionary `Dict`,
 148   or defining *type synonym* of *type classes*,
 149   or merging *type constraints*.
 150 * `DataKinds` for type-level data structures (eg. *type-level lists*).
 151 * `DefaultSignatures` for providing identity transformations of terms,
 152   and thus avoid boilerplate code when a transformation
 153   does not need to alter all semantics.
 154   Almost as explained in [Reducing boilerplate in finally tagless style](https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate).
 155 * `GADTs` for knowing types by pattern-matching terms,
 156   or building terms by using type classes.
 157 * `PolyKinds` for avoiding a lot of uses of `Proxy`.
 158 * `Rank2Types` or `ExistentialQuantification` for parsing `GADT`s.
 159 * `TypeApplications` for having a more concise syntax
 160   to build `Type` (eg. `tyConst `Bool`).
 161 * `TypeFamilies` for type-level programming.
 162 * `TypeInType` (introduced in GHC 8.0.1)
 163   for `Type` to also bind a kind equality for the type `t` it encodes.
 164   Which makes the *type application* (`TyApp`)
 165   give us an *arrow kind* for the Haskell *type constructor*
 166   it applies an Haskell type to, releaving me from tricky workarounds.
 167 * `UndecidableInstances` to relax the checks that the type-level programming does terminate.
 168
 169 # Bugs
 170
 171 There are some of them hidding in there,
 172 and the whole thing is far from being perfect…
 173 Your comments, problem reports, or questions, are welcome!
 174 You have my email address, so… just send me some emails :]
 175
 176 # To do
 177
 178 * Study to which point *type inferencing* is doable,
 179   now that `Type` is powerful enough to contain `TyVar`s.
 180 * Study to which point error messages can be improved,
 181   now that there is a `Source` carried through all `Kind`s or `Type`s,
 182   it should enable some nice reports.
 183   Still, a lot of work and testing remain to be done,
 184   and likely some ideas to find too…
 185 * Add more terms in [symantic-lib](https://hackage.haskell.org/package/symantic-lib).
 186 * Add more transformations.
 187 * Study how to list class instances.
 188 * Study where to put `INLINE`, `INLINEABLE` or `SPECIALIZE` pragmas.
 189 * Study how to support *rank-N polymorphic types*,
 190   special cases can likely use the *boxed polymorphism* workaround,
 191   but even if GHC were supporting *impredicative types*,
 192   I'm currently clueless about how to do this.