1 author: Julien Moutinho <julm+symantic@autogeree.net>
2 bug-reports: Julien Moutinho <julm+symantic@autogeree.net>
9 Library for composing, typing, compiling, transforming and interpreting
10 a custom DSL (Domain-Specific Language) expressing a subset of GHC's Haskell.
11 Its main goal is to enable the runtime handling of terms typed
12 according to some compile-time defined types.
13 The idea being that the more complex logic shall remain coded in Haskell
14 and then this library used to project an interface into a DSL
15 giving runtime users the flexibility to write simple programs suited to their needs.
19 * Enabling runtime users to enter some Haskell-like expressions
20 without using all the weight and slowness of GHC
21 at runtime (eg. by using <https://hackage.haskell.org/package/hint hint>).
22 * Limiting those expressions to be built only from well-controlled expressions.
23 * Run some analyzes/optimizations on those well-controlled expressions.
27 Please be aware that despite its using of powerful ideas from clever people,
28 this remains a fund-less single-person experimental library.
29 Meaning that it is all but heavily tested and documented,
30 does not have a strong commitment to preserving backward compatibility,
31 and can just die without notice.
32 Its version follows the <http://www.haskell.org/haskellwiki/Package_versioning_policy PVP>,
33 so you may want to use upper-bounds in @build-depends@.
34 This said, hope you'll enjoy the tool :)
38 Reading the boring @Test.hs@ files should give you enough examples
39 to understand how to use this library,
40 and reading some of the repetitively boring
41 and painfully repetitive @Lib/*.hs@ files
42 should give you some templates and the general pattern
43 to let you extend this library with your own symantics.
45 The @Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser
46 and a default grammar somehow sticking to Haskell's, but staying context-free
47 (so in particular: insensitive to the indentation).
48 This grammar, itself written as a symantic embedded DSL,
49 can be reused to build another one,
50 is not bound to a specific parser,
51 and can produce its EBNF rendition.
56 To encode terms in the <http://okmij.org/ftp/tagless-final/ Tagless-Final> way
57 (aka. the /symantic/ way)
58 i.e. to use a /class/ to encode the /syntax/ of terms (eg. 'Sym_Bool')
59 and /class instances/ on a dedicated type to encode their /semantics/
60 (eg. @(Sym_Bool HostI)@ interprets a term as a value of its type
61 in the host language (Haskell here),
62 or @(Sym_Bool TextI)@ interprets a term as a textual rendition, etc.).
64 DSL are then composed by selecting those symantic /classes/.
65 When using symantics for an embedded DSL
66 those /classes/ are all inferred by GHC from the terms used,
67 provided that the @NoMonomorphismRestriction@ extension is on.
68 Otherwise, when using symantics for a non-embedded DSL
69 — the whole point of this library — the /classes/ composing the DSL
70 are selected manually at GHC's compile-time,
71 through the /type-level list/ given to 'compile'.
73 Moreover, the terms are parameterized by the type of the value they encode,
74 in order to get the same type safety as with plain Haskell values.
75 Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@
76 instead of just @(* -> Constraint)@.
78 Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach,
79 meaning that they directly reuse GHC's internal machinery
80 to abstract or instantiate variables,
81 which I think is by far the most efficient and simplest way of doing it
82 (no DeBruijn encoding nor <https://hackage.haskell.org/package/bound bound>'s monads).
84 * __Singleton for any type__.
85 To typecheck terms using a @(Type cs h)@ @GADT@ which acts
86 as a /singleton type/ for any Haskell type @h@
87 buildable by composing the /type constants/ @cs@,
88 each one wrapped inside a @Proxy@ to fit into a common /type-level list/
89 (eg. @cs ~ [Proxy Bool, Proxy (->), Proxy Eq]@).
91 * __Extensible data type__.
92 To inject a type into a /type-level list/
93 or project a /type-level list/ onto a type,
94 to compose an /extensible data type/
95 (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,
96 that a parser can build and then give to 'compile').
97 This type-level programming requires @UndecidableInstances@,
98 but not @OverlappingInstances@.
100 There is a similarity with
101 <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>
102 (see for instance <https://hackage.haskell.org/package/compdata compdata>
103 or <https://hackage.haskell.org/package/syntactic syntactic>).
104 Those also enable to compose a DSL using some machinery
105 based upon (co)free(r) (co)monads and (cata|ana)morphisms.
106 Which library fits best your problem domain and brain is for you to judge :)
107 On that topic, see also:
108 <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.
110 Here, I just came up using /type-level lists/ by hacking
111 <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.
113 * __Extensible class__.
114 To recurse on a /type-level list/ through
115 /class instances/ to compose an /extensible class/
116 (eg. 'CompileR' gathering the 'CompileI' /class instances/,
117 or the more tricky 'TermO' /type-level list-zipper/
118 gathering 'Sym_of_Iface' /class instances/
119 while providing in scope the current 'Sym_of_Iface'
120 within each 'TermO' built in a 'CompileI' /class instance/).
124 * @GADTs@ for knowing types by pattern-matching terms,
125 or building terms by using type classes.
126 * @Rank2Types@ for parsing @GADT@s.
127 * @TypeInType@ (introduced in GHC 8.0.1)
128 for 'Type' to also bind a kind equality for the type @h@ it encodes.
129 Which makes the /type application/ (':$')
130 give us an /arrow kind/ for the Haskell /type constructor/
131 it applies an Haskell type to, releaving me from tricky workarounds.
132 * @ConstraintKinds@ for @cs@ to contain 'Constraint's,
133 or defining /type synonym/ of /type classes/,
134 or merging /type constraints/.
135 * @DataKinds@ for type-level data structures (eg. /type-level lists/).
136 * @TypeFamilies@ for type-level programming.
137 * @UndecidableInstances@ for type-level programming
138 that may never terminate.
139 * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.
140 * @TypeApplications@ for having a more concise syntax
141 to build 'Type' (eg. @ty \@Bool@).
142 * @DefaultSignatures@ for providing identity transformations of terms,
143 and thus avoid boilerplate code when a transformation
144 does not need to alter all semantics.
145 As explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.
149 Your comments, problem reports, or questions are welcome!
151 You have my email address, so… just send me some emails :]
155 * Study to which point /type inferencing/ is doable,
156 so that it would improve the current /type checking/,
157 and remove some type annotations in the DSL.
158 Currently each /lambda abstraction/ must have its variable explicitely typed,
159 and terms must be called with enough arguments to typecheck,
160 be it term arguments (for instance
161 @(+) :: Num a => a -> a -> a@ needs at least one term argument to check @Num a@)
162 or type arguments (for instance
163 @return :: Monad m => a -> m a@ needs a type argument to check @Monad m@).
164 * Study to which point error messages can be improved.
165 * A lot of common terms should be added in @Lib.*@ modules.
166 Maybe as separate packages to limit dependencies.
167 * No transformation is implemented so far,
168 maybe there should be some, at least as examples
169 to demonstrate their power.
170 * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.
175 license-file: COPYING
176 maintainer: Julien Moutinho <julm+symantic@autogeree.net>
178 stability: experimental
179 synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
180 tested-with: GHC==8.0.1
181 -- PVP: +-+------- breaking API changes
182 -- | | +----- non-breaking API additions
183 -- | | | +--- code changes with no API change
184 version: 4.0.0.20170202
186 Source-Repository head
187 location: git://git.autogeree.net/symantic
198 MultiParamTypeClasses
209 -fwarn-incomplete-patterns
211 -fprint-explicit-kinds
212 default-language: Haskell2010
215 Language.Symantic.Compiling
216 Language.Symantic.Compiling.Term
217 Language.Symantic.Compiling.Term.Grammar
218 Language.Symantic.Helper.Data.Type.List
219 Language.Symantic.Helper.Data.Type.Peano
220 Language.Symantic.Interpreting
221 Language.Symantic.Interpreting.Dup
222 Language.Symantic.Interpreting.Host
223 Language.Symantic.Interpreting.Text
224 Language.Symantic.Lib
225 Language.Symantic.Lib.Alternative
226 Language.Symantic.Lib.Applicative
227 Language.Symantic.Lib.Bool
228 Language.Symantic.Lib.Char
229 Language.Symantic.Lib.Either
230 Language.Symantic.Lib.Eq
231 Language.Symantic.Lib.Foldable
232 Language.Symantic.Lib.Functor
233 Language.Symantic.Lib.IO
234 Language.Symantic.Lib.If
235 Language.Symantic.Lib.Int
236 Language.Symantic.Lib.Integer
237 Language.Symantic.Lib.Integral
238 Language.Symantic.Lib.Lambda
239 Language.Symantic.Lib.List
240 Language.Symantic.Lib.Map
241 Language.Symantic.Lib.Maybe
242 Language.Symantic.Lib.Monad
243 Language.Symantic.Lib.MonoFoldable
244 Language.Symantic.Lib.MonoFunctor
245 Language.Symantic.Lib.Monoid
246 Language.Symantic.Lib.NonNull
247 Language.Symantic.Lib.Num
248 Language.Symantic.Lib.Ord
249 Language.Symantic.Lib.Sequences
250 Language.Symantic.Lib.Show
251 Language.Symantic.Lib.Text
252 Language.Symantic.Lib.Traversable
253 Language.Symantic.Lib.Tuple2
254 Language.Symantic.Lib.Unit
255 Language.Symantic.Parsing
256 Language.Symantic.Parsing.EBNF
257 Language.Symantic.Parsing.Grammar
258 Language.Symantic.Parsing.Token
259 Language.Symantic.Transforming
260 Language.Symantic.Transforming.Trans
261 Language.Symantic.Typing
262 Language.Symantic.Typing.Constant
263 Language.Symantic.Typing.Constraint
264 Language.Symantic.Typing.Family
265 Language.Symantic.Typing.Kind
266 Language.Symantic.Typing.Type
275 Test-Suite symantic-test
276 type: exitcode-stdio-1.0
281 MultiParamTypeClasses
282 NoMonomorphismRestriction
289 default-language: Haskell2010
291 -fwarn-incomplete-patterns
296 -- -fmax-simplifier-iterations=0
297 -- -fprint-explicit-kinds
298 hs-source-dirs: Language/Symantic
327 type: exitcode-stdio-1.0
334 MultiParamTypeClasses
348 -main-is Parsing.EBNF.Print
349 main-is: Parsing/EBNF/Print.hs
350 default-language: Haskell2010
351 hs-source-dirs: Language/Symantic