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  .
  68  __Usage__
  69  .
  70  Please pick in <https://hackage.haskell.org/package/symantic-lib symantic-lib>
  71  a few specific @Lib/*.hs@ files near what you want to do
  72  and the corresponding @Lib\/*/Test.hs@ file,
  73  if any in the <git://git.autogeree.net/symantic Git repository>,
  74  to learn by examples how to use this library.
  75  .
  76  Those @Lib\/*/Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser
  77  (see @Grammar/Megaparsec.hs@) and a default grammar somehow sticking to Haskell's,
  78  but staying context-free (so in particular: insensitive to the indentation),
  79  and supporting prefix and postfix operators.
  80  This grammar — itself written as a symantic embedded DSL
  81  with <https://hackage.haskell.org/package/symantic-grammar symantic-grammar> —
  82  can be reused to build other ones, is not bound to a specific parser,
  83  and can produce its own EBNF rendition.
  84  .
  85  __Acknowledgements__
  86  .
  87  This library would probably be much worse than it is
  88  without the following seminal works:
  89  .
  90  * <http://okmij.org/ftp/tagless-final/ Finally Tagless> by Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan.
  91  * <http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf Dependent Types in Haskell> by Richard A. Eisenberg.
  92  .
  93  __Main ideas__
  94  .
  95  * __Symantic DSL__.
  96    Terms are encoded in the <http://okmij.org/ftp/tagless-final/ 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 <https://hackage.haskell.org/package/bound 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  -- NOTE: no longer used.
 144  -- * __Extensible data type__.
 145  --   To inject a type into a /type-level list/
 146  --   or project a /type-level list/ onto a type,
 147  --   to compose an /extensible data type/
 148  --   (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,
 149  --   that a parser can build and then give to 'compile').
 150  --   This type-level programming requires @UndecidableInstances@,
 151  --   but not @OverlappingInstances@.
 152  --
 153  --   There is a similarity with
 154  --   <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>
 155  --   (see for instance <https://hackage.haskell.org/package/compdata compdata>
 156  --   or <https://hackage.haskell.org/package/syntactic syntactic>).
 157  --   Those also enable to compose a DSL using some machinery
 158  --   based upon (co)free(r) (co)monads and (cata|ana)morphisms.
 159  --   Which library fits best your problem domain and brain is for you to judge :)
 160  --   On that topic, see also:
 161  --   <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.
 162  --
 163  -- Here, I just came up using /type-level lists/ by hacking
 164  -- <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.
 165  .
 166  __Main extensions__
 167  .
 168  * @AllowAmbiguousTypes@ for avoiding a lot of uses of 'Proxy'.
 169  * @ConstraintKinds@ for /type lists/ to contain 'Constraint's,
 170    or reifying any 'Constraint' as an explicit dictionary 'Dict',
 171    or defining /type synonym/ of /type classes/,
 172    or merging /type constraints/.
 173  * @DataKinds@ for type-level data structures (eg. /type-level lists/).
 174  * @DefaultSignatures@ for providing identity transformations of terms,
 175    and thus avoid boilerplate code when a transformation
 176    does not need to alter all semantics.
 177    Almost as explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.
 178  * @GADTs@ for knowing types by pattern-matching terms,
 179    or building terms by using type classes.
 180  * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.
 181  * @Rank2Types@ or @ExistentialQuantification@ for parsing @GADT@s.
 182  * @TypeApplications@ for having a more concise syntax
 183    to build 'Type' (eg. 'tyConst'@ @\@Bool).
 184  * @TypeFamilies@ for type-level programming.
 185  * @TypeInType@ (introduced in GHC 8.0.1)
 186    for 'Type' to also bind a kind equality for the type @t@ it encodes.
 187    Which makes the /type application/ ('TyApp')
 188    give us an /arrow kind/ for the Haskell /type constructor/
 189    it applies an Haskell type to, releaving me from tricky workarounds.
 190  * @UndecidableInstances@ for type-level programming that may never terminate.
 191  .
 192  __Bugs__
 193  .
 194  There are some of them hidding in there,
 195  and the whole thing is far from being perfect…
 196  Your comments, problem reports, or questions, are welcome!
 197  You have my email address, so… just send me some emails :]
 198  .
 199  __To do__
 200  .
 201  * Study to which point /type inferencing/ is doable,
 202    now that 'Type' is powerful enough to contain 'TyVar's.
 203  * Study to which point error messages can be improved,
 204    now that there is a 'Source' carried through all 'Kind's or 'Type's,
 205    it should enable some nice reports.
 206    Still, a lot of work and testing remain to be done,
 207    and likely some ideas to find too…
 208  * Add more terms in <https://hackage.haskell.org/package/symantic-lib symantic-lib>.
 209  * Add more transformations.
 210  * Study how to integrate types into the module system.
 211  * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.
 212  * Study how to support /rank-N polymorphic types/,
 213    special cases can likely use the /boxed polymorphism/ workaround,
 214    but even if GHC were supporting /impredicative types/,
 215    I'm currently clueless about how to do this.
 216 extra-source-files:
 217 extra-tmp-files:
 218 -- homepage:
 219 license: GPL-3
 220 license-file: COPYING
 221 maintainer: Julien Moutinho <julm+symantic@autogeree.net>
 222 name: symantic
 223 stability: experimental
 224 synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
 225 tested-with: GHC==8.0.2
 226 -- PVP:  +-+------- breaking API changes
 227 --       | | +----- non-breaking API additions
 228 --       | | | +--- code changes with no API change
 229 version: 6.0.0.20170623
 230
 231 Source-Repository head
 232   location: git://git.autogeree.net/symantic
 233   type:     git
 234
 235 Library
 236   default-extensions:
 237     DataKinds
 238     DefaultSignatures
 239     FlexibleContexts
 240     FlexibleInstances
 241     LambdaCase
 242     MultiParamTypeClasses
 243     NamedFieldPuns
 244     OverloadedStrings
 245     Rank2Types
 246     ScopedTypeVariables
 247     StandaloneDeriving
 248     TupleSections
 249     TypeApplications
 250     TypeFamilies
 251     TypeOperators
 252   ghc-options: -Wall
 253                -fno-warn-tabs
 254   default-language: Haskell2010
 255   exposed-modules:
 256     Language.Symantic
 257     Language.Symantic.Compiling
 258     Language.Symantic.Compiling.Beta
 259     Language.Symantic.Compiling.Grammar
 260     Language.Symantic.Compiling.Module
 261     Language.Symantic.Compiling.Read
 262     Language.Symantic.Compiling.Term
 263     Language.Symantic.Interpreting
 264     Language.Symantic.Interpreting.Dup
 265     Language.Symantic.Interpreting.Eval
 266     Language.Symantic.Interpreting.View
 267     Language.Symantic.Transforming
 268     Language.Symantic.Transforming.Beta
 269     Language.Symantic.Transforming.Trans
 270     Language.Symantic.Typing
 271     Language.Symantic.Typing.Document
 272     Language.Symantic.Typing.Grammar
 273     Language.Symantic.Typing.Kind
 274     Language.Symantic.Typing.List
 275     Language.Symantic.Typing.Peano
 276     Language.Symantic.Typing.Read
 277     Language.Symantic.Typing.Show
 278     Language.Symantic.Typing.Type
 279     Language.Symantic.Typing.Unify
 280     Language.Symantic.Typing.Variable
 281   build-depends:
 282     base >= 4.6 && < 5
 283     , containers
 284     , ghc-prim
 285     , mono-traversable
 286     , symantic-grammar
 287     , symantic-document
 288     , transformers
 289     , text