symantic 6.3.0.20170703 → 6.3.0.20170807

raw patch · 3 files changed

+196/−3 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Language/Symantic/Typing/Kind.hs +2/−2
• README.md +192/−0
• symantic.cabal +2/−1

@@ -51,7 +51,7 @@ class KindOf (a::kt -> K.Type) where 	kindOf :: a t -> Kind (SourceOf (a t)) kt --- * Type 'Kind'Inj+-- * Type 'KindInj' -- | Implicit 'Kind'. -- -- NOTE: GHC-8.0.1's bug <https://ghc.haskell.org/trac/ghc/ticket/12933 #12933>@@ -69,7 +69,7 @@  Kind src k kindInj = kindInjP @(Ty_of_Type k) (noSource @src) --- ** Type 'KindP'Inj+-- ** Type 'KindInjP' class KindInjP k where 	kindInjP :: src -> Kind src (Type_of_Ty k) instance KindInjP K.Constraint where

@@ -0,0 +1,192 @@+# 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.+* [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.+* [Typeable](https://ghc.haskell.org/trac/ghc/wiki/Typeable) by Ben Gamari and others.++# 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.

@@ -7,6 +7,7 @@              typing, compiling, transforming and interpreting              a custom DSL (Domain-Specific Language)              expressing a subset of GHC's Haskell type system.+extra-doc-files: README.md extra-source-files: extra-tmp-files: -- homepage: @@ -20,7 +21,7 @@ -- PVP:  +-+------- breaking API changes --       | | +----- non-breaking API additions --       | | | +--- code changes with no API change-version: 6.3.0.20170703+version: 6.3.0.20170807  Source-Repository head   location: git://git.autogeree.net/symantic