symantic/symantic.cabal

   1 author: Julien Moutinho <julm+symantic@autogeree.net>
   2 bug-reports: Julien Moutinho <julm+symantic@autogeree.net>
   3 build-type: Simple
   4 cabal-version: >= 1.24
   5 category: Language
   6 description:
   7  __Description__
   8  .
   9  This is an experimental library for composing, parsing, typing, compiling, transforming and interpreting
  10  a custom DSL (Domain-Specific Language) expressing
  11  a subset of GHC's Haskell type system:
  12  .
  13  * /first class functions/ (aka. /lambdas/),
  14  * chosen /monomorphic types/ (like 'Bool' or 'Maybe'),
  15  * chosen /rank-1 polymorphic types/ (like @(@'Maybe'@ a)@),
  16  * chosen /type class instances/,
  17  * chosen /type family instances/,
  18  * and chosen /type constraints/;
  19  .
  20  where "chosen X" means declared in Haskell
  21  and selected when composing the DSL.
  22  .
  23  In particular, this library is currently not able to:
  24  .
  25  * do /type inferencing/ for the argument of /lambdas/
  26    (they must all be explicitely annotated, aka. /Church-style/),
  27  * do /pattern matching/ (aka. /case/) (but /Church-encoding/ functions are often enough),
  28  * do /rank-N polymorphic types/ (aka. /non-prenex forall/, like @(forall s. ST s a) -> a@).
  29  .
  30  And by itself, the DSL is only able to define new terms to be interpreted,
  31  no new types, or other type-level structures.
  32  .
  33  __Warning__
  34  .
  35  Please be aware that despite its using of powerful ideas from clever people,
  36  this remains a FUND-LESS SINGLE-PERSON EXPERIMENTAL LIBRARY.
  37  Meaning that it IS NOT heavily tested and documented,
  38  DOES NOT have a strong commitment to preserving backward compatibility,
  39  MAY FAIL to comply with the <http://www.haskell.org/haskellwiki/Package_versioning_policy PVP>,
  40  and CAN die without notice.
  41  You've been warned.
  42  .
  43  __Use cases__
  44  .
  45  The main goal of this library is to enable the runtime interpretation of terms,
  46  type-checked according to some types defined at composing-time (ie. GHC's compile-time).
  47  .
  48  Using a DSL enables to limit expressiveness in order to ease analysis.
  49  Here the idea is that the more complex logic shall remain written in Haskell,
  50  and then this library used to project an interface into a DSL
  51  (using GHC's Haskell as a FFI (Foreign Function Interface)).
  52  This in order to give runtime users the flexibility
  53  to write programs not requiring a full-blown Haskell compiler,
  54  yet enabling enough flexibility to let them express complex needs
  55  with a reasonably advanced type-safe way
  56  and a controlled environment of primitives.
  57  .
  58  Typical use cases:
  59  .
  60  * Enabling runtime users to enter some Haskell-like expressions
  61    (maybe with a more convenient syntax wrt. the domain problem)
  62    without using at runtime all the heavy machinery and ecosystem of GHC
  63    (eg. by using <https://hackage.haskell.org/package/hint hint>),
  64    but still leaning on primitive functions coded in GHC's Haskell.
  65  * Limiting those expressions to be built from well-controlled expressions only.
  66  * Run some analyzes/optimizations on those well-controlled expressions.
  67  * Report errors specific to the domain problem.
  68  .
  69  __Usage__
  70  .
  71  Please pick in <https://hackage.haskell.org/package/symantic-lib symantic-lib>
  72  a few specific @Lib/*.hs@ files near what you want to do
  73  and the corresponding @Lib\/*/Test.hs@ file,
  74  if any in the <git://git.autogeree.net/symantic Git repository>,
  75  to learn by examples how to use this library.
  76  .
  77  Those @Lib\/*/Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser
  78  (see @Grammar/Megaparsec.hs@) and a default grammar somehow sticking to Haskell's,
  79  but staying context-free (so in particular: insensitive to the indentation),
  80  and supporting prefix and postfix operators.
  81  This grammar — itself written as a symantic embedded DSL
  82  with <https://hackage.haskell.org/package/symantic-grammar symantic-grammar> —
  83  can be reused to build other ones, is not bound to a specific parser,
  84  and can produce its own EBNF rendition.
  85  .
  86  __Acknowledgements__
  87  .
  88  This library would probably be much worse than it is
  89  without the following seminal works:
  90  .
  91  * <http://okmij.org/ftp/tagless-final/ Finally Tagless> by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
  92  * <http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf Dependent Types in Haskell> by Richard A. Eisenberg.
  93  .
  94  __Main ideas__
  95  .
  96  * __Symantic DSL__.
  97    Terms are encoded in the <http://okmij.org/ftp/tagless-final/ Tagless-Final> way (aka. the /symantic/ way)
  98    which leverages the /type class/ system of Haskell — instead of using /data types/ — to form an embedded DSL.
  99    More specifically, a /class/ encodes the /syntax/ of terms (eg. 'Sym_Bool')
 100    and its /class instances/ on a dedicated type encodes their /semantics/
 101    (eg. @(Sym_Bool Eval)@ interprets a term as a value of its type
 102    in the host language ('Bool' in Haskell here),
 103    or @(Sym_Bool View)@ interprets a term as a textual rendition, etc.).
 104
 105    DSL are then composed\/extended by selecting those symantic /classes/
 106    (and in an embedded DSL those could even be automatically inferred,
 107    when @NoMonomorphismRestriction@ is on).
 108    Otherwise, when using symantics for a non-embedded DSL
 109    — the whole point of this library — the /classes/ composing the DSL
 110    are selected manually at GHC's compile-time,
 111    through the /type-level list/ @ss@ given to 'readTerm'.
 112
 113    Moreover, those symantic @term@s are parameterized by the type of the value they encode,
 114    in order to get the same type safety as with plain Haskell values.
 115    Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@
 116    instead of just @(* -> Constraint)@.
 117
 118    Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach,
 119    meaning that they directly reuse GHC's internal machinery
 120    to abstract or instantiate variables,
 121    which I think is by far the most efficient and simplest way of doing it
 122    (no (generalized or not) DeBruijn encoding
 123    like in <https://hackage.haskell.org/package/bound bound>'s @Monad@s).
 124
 125  * __Singleton for any type__.
 126    To typecheck terms using a @(@'Type'@ src vs t)@ which acts as a /singleton type/
 127    for any Haskell /type index/ @t@ of any kind,
 128    which is made possible with the dependant Haskell extensions:
 129    especially @TypeFamilies@, @GADTs@ and @TypeInType@.
 130
 131  * __Type constants using 'Typeable'__.
 132    /Type constant/ could be introduced by indexing them amongst a /type-level list/,
 133    but since they are /monomorphic types/, using 'Typeable' simplifies
 134    the machinery, and is likely more space/time efficient, including at GHC-compile-time.
 135
 136  * __Type variables using a type-level list__.
 137    Handling /type variables/ is done by indexing them amongst a @vs@ /type-level list/,
 138    where each /type variable/ is wrapped inside a @Proxy@ to handle different kinds.
 139    Performing a substitution (in 'substVar') preserves the /type index/ @t@,
 140    which is key for preserving any associated 'Term'.
 141    Unifying /type variables/ is done with 'unsafeCoerce' (in 'unifyType'),
 142    which I think is necessary and likely safe.
 143
 144  -- NOTE: no longer used.
 145  -- * __Extensible data type__.
 146  --   To inject a type into a /type-level list/
 147  --   or project a /type-level list/ onto a type,
 148  --   to compose an /extensible data type/
 149  --   (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,
 150  --   that a parser can build and then give to 'compile').
 151  --   This type-level programming requires @UndecidableInstances@,
 152  --   but not @OverlappingInstances@.
 153  --
 154  --   There is a similarity with
 155  --   <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>
 156  --   (see for instance <https://hackage.haskell.org/package/compdata compdata>
 157  --   or <https://hackage.haskell.org/package/syntactic syntactic>).
 158  --   Those also enable to compose a DSL using some machinery
 159  --   based upon (co)free(r) (co)monads and (cata|ana)morphisms.
 160  --   Which library fits best your problem domain and brain is for you to judge :)
 161  --   On that topic, see also:
 162  --   <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.
 163  --
 164  -- Here, I just came up using /type-level lists/ by hacking
 165  -- <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.
 166  .
 167  __Main extensions__
 168  .
 169  * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'.
 170  * @ConstraintKinds@ for /type lists/ to contain 'Constraint's,
 171    or reifying any 'Constraint' as an explicit dictionary 'Dict',
 172    or defining /type synonym/ of /type classes/,
 173    or merging /type constraints/.
 174  * @DataKinds@ for type-level data structures (eg. /type-level lists/).
 175  * @DefaultSignatures@ for providing identity transformations of terms,
 176    and thus avoid boilerplate code when a transformation
 177    does not need to alter all semantics.
 178    Almost as explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.
 179  * @GADTs@ for knowing types by pattern-matching terms,
 180    or building terms by using type classes.
 181  * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.
 182  * @Rank2Types@ or @ExistentialQuantification@ for parsing @GADT@s.
 183  * @TypeApplications@ for having a more concise syntax
 184    to build 'Type' (eg. 'tyConst'@ @\@Bool).
 185  * @TypeFamilies@ for type-level programming.
 186  * @TypeInType@ (introduced in GHC 8.0.1)
 187    for 'Type' to also bind a kind equality for the type @t@ it encodes.
 188    Which makes the /type application/ ('TyApp')
 189    give us an /arrow kind/ for the Haskell /type constructor/
 190    it applies an Haskell type to, releaving me from tricky workarounds.
 191  * @UndecidableInstances@ to relax the checks that the type-level programming does terminate.
 192  .
 193  __Bugs__
 194  .
 195  There are some of them hidding in there,
 196  and the whole thing is far from being perfect…
 197  Your comments, problem reports, or questions, are welcome!
 198  You have my email address, so… just send me some emails :]
 199  .
 200  __To do__
 201  .
 202  * Study to which point /type inferencing/ is doable,
 203    now that 'Type' is powerful enough to contain 'TyVar's.
 204  * Study to which point error messages can be improved,
 205    now that there is a 'Source' carried through all 'Kind's or 'Type's,
 206    it should enable some nice reports.
 207    Still, a lot of work and testing remain to be done,
 208    and likely some ideas to find too…
 209  * Add more terms in <https://hackage.haskell.org/package/symantic-lib symantic-lib>.
 210  * Add more transformations.
 211  * Study how to integrate types into the module system.
 212  * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.
 213  * Study how to support /rank-N polymorphic types/,
 214    special cases can likely use the /boxed polymorphism/ workaround,
 215    but even if GHC were supporting /impredicative types/,
 216    I'm currently clueless about how to do this.
 217 extra-source-files:
 218 extra-tmp-files:
 219 -- homepage:
 220 license: GPL-3
 221 license-file: COPYING
 222 maintainer: Julien Moutinho <julm+symantic@autogeree.net>
 223 name: symantic
 224 stability: experimental
 225 synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
 226 tested-with: GHC==8.0.2
 227 -- PVP:  +-+------- breaking API changes
 228 --       | | +----- non-breaking API additions
 229 --       | | | +--- code changes with no API change
 230 version: 6.1.0.20170624
 231
 232 Source-Repository head
 233   location: git://git.autogeree.net/symantic
 234   type:     git
 235
 236 Library
 237   default-extensions:
 238     DataKinds
 239     DefaultSignatures
 240     FlexibleContexts
 241     FlexibleInstances
 242     LambdaCase
 243     MultiParamTypeClasses
 244     NamedFieldPuns
 245     OverloadedStrings
 246     Rank2Types
 247     ScopedTypeVariables
 248     StandaloneDeriving
 249     TupleSections
 250     TypeApplications
 251     TypeFamilies
 252     TypeOperators
 253   ghc-options: -Wall
 254                -fno-warn-tabs
 255   default-language: Haskell2010
 256   exposed-modules:
 257     Language.Symantic
 258     Language.Symantic.Compiling
 259     Language.Symantic.Compiling.Beta
 260     Language.Symantic.Compiling.Grammar
 261     Language.Symantic.Compiling.Module
 262     Language.Symantic.Compiling.Read
 263     Language.Symantic.Compiling.Term
 264     Language.Symantic.Interpreting
 265     Language.Symantic.Interpreting.Dup
 266     Language.Symantic.Interpreting.Eval
 267     Language.Symantic.Interpreting.View
 268     Language.Symantic.Transforming
 269     Language.Symantic.Transforming.Beta
 270     Language.Symantic.Transforming.Trans
 271     Language.Symantic.Typing
 272     Language.Symantic.Typing.Document
 273     Language.Symantic.Typing.Grammar
 274     Language.Symantic.Typing.Kind
 275     Language.Symantic.Typing.List
 276     Language.Symantic.Typing.Peano
 277     Language.Symantic.Typing.Read
 278     Language.Symantic.Typing.Show
 279     Language.Symantic.Typing.Type
 280     Language.Symantic.Typing.Unify
 281     Language.Symantic.Typing.Variable
 282   build-depends:
 283     base >= 4.6 && < 5
 284     , containers
 285     , ghc-prim
 286     , mono-traversable
 287     , symantic-grammar
 288     , symantic-document
 289     , transformers
 290     , text