]> Git — Sourcephile - haskell/symantic.git/blob - symantic/symantic.cabal
Complexify the type system to support rank-1 polymorphic types and terms.
[haskell/symantic.git] / 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 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 simpler programs suited to their needs.
16 .
17 Typical use cases:
18 .
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 from well-controlled expressions only.
23 * Run some analyzes/optimizations on those well-controlled expressions.
24 .
25 __Warning__
26 .
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 (the Crohn infection I carry being only one of the many reasons).
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, I hope you'll enjoy the tool, or at least fish in it some inspiring ideas,
35 'cause I had to smash those bytes with my poor head, day and night,
36 a whole year of my life, to scult them as they currently are :P
37 .
38 __Usage__
39 .
40 Reading the boring @Test.hs@ files
41 of <https://hackage.haskell.org/package/symantic-lib symantic-lib>
42 should give you enough examples
43 to understand how to use this library,
44 and reading some of the repetitively boring
45 and painfully repetitive @Lib/*.hs@ files
46 of <https://hackage.haskell.org/package/symantic-lib symantic-lib>
47 should give you some templates and the general pattern
48 to let you extend this library with your own symantics.
49 .
50 The @Test.hs@ files use <https://hackage.haskell.org/package/megaparsec megaparsec> as parser
51 and a default grammar somehow sticking to Haskell's, but staying context-free
52 (so in particular: insensitive to the indentation).
53 This grammar, itself written as a symantic embedded DSL,
54 can be reused to build another one,
55 is not bound to a specific parser,
56 and can produce its EBNF rendition.
57 .
58 __Main ideas__
59 .
60 * __Symantic DSL__.
61 To encode terms in the <http://okmij.org/ftp/tagless-final/ Tagless-Final> way
62 (aka. the /symantic/ way)
63 i.e. to use a /class/ to encode the /syntax/ of terms (eg. 'Sym_Bool')
64 and /class instances/ on a dedicated type to encode their /semantics/
65 (eg. @(Sym_Bool HostI)@ interprets a term as a value of its type
66 in the host language (Haskell here),
67 or @(Sym_Bool TextI)@ interprets a term as a textual rendition, etc.).
68
69 DSL are then composed by selecting those symantic /classes/.
70 When using symantics for an embedded DSL
71 those /classes/ are all inferred by GHC from the terms used,
72 provided that the @NoMonomorphismRestriction@ extension is on.
73 Otherwise, when using symantics for a non-embedded DSL
74 — the whole point of this library — the /classes/ composing the DSL
75 are selected manually at GHC's compile-time,
76 through the /type-level list/ given to 'compile'.
77
78 Moreover, the terms are parameterized by the type of the value they encode,
79 in order to get the same type safety as with plain Haskell values.
80 Hence the symantic /classes/ have the higher kind: @((* -> *) -> Constraint)@
81 instead of just @(* -> Constraint)@.
82
83 Amongst those symantics, 'Sym_Lambda' introduces /lambda abstractions/ by an higher-order approach,
84 meaning that they directly reuse GHC's internal machinery
85 to abstract or instantiate variables,
86 which I think is by far the most efficient and simplest way of doing it
87 (no DeBruijn encoding nor <https://hackage.haskell.org/package/bound bound>'s monads).
88
89 * __Singleton for any type__.
90 To typecheck terms using a @(Type cs h)@ @GADT@ which acts
91 as a /singleton type/ for any Haskell type @h@
92 buildable by composing the /type constants/ @cs@,
93 each one wrapped inside a @Proxy@ to fit into a common /type-level list/
94 (eg. @cs ~ [Proxy Bool, Proxy (->), Proxy Eq]@).
95
96 * __Embed 'Term' in 'Type'__.
97 To handle quantified (rank-1 only) and qualified terms,
98 by using a rank-2 polymorphic function to introduce a bound type variable ('TyQuant'),
99 and a function to pass the proof of a 'Constraint' ('TyQual').
100 This is possible by loosing the type indexing of 'Type',
101 because so far it is not possible to index quantified and qualified types
102 (which would require a powerful /impredicative polymorphism/).
103
104 * __Extensible data type__.
105 To inject a type into a /type-level list/
106 or project a /type-level list/ onto a type,
107 to compose an /extensible data type/
108 (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/,
109 that a parser can build and then give to 'compile').
110 This type-level programming requires @UndecidableInstances@,
111 but not @OverlappingInstances@.
112
113 There is a similarity with
114 <http://dx.doi.org/10.1017/S0956796808006758 Data types à la carte>
115 (see for instance <https://hackage.haskell.org/package/compdata compdata>
116 or <https://hackage.haskell.org/package/syntactic syntactic>).
117 Those also enable to compose a DSL using some machinery
118 based upon (co)free(r) (co)monads and (cata|ana)morphisms.
119 Which library fits best your problem domain and brain is for you to judge :)
120 On that topic, see also:
121 <https://www.youtube.com/watch?v=qaAKRxO21fU Stop Paying for Free Monads>.
122
123 Here, I just came up using /type-level lists/ by hacking
124 <https://hackage.haskell.org/package/glambda glambda>'s @Elem@.
125
126 * __Extensible class__.
127 To recurse on a /type-level list/ through
128 /class instances/ to compose an /extensible class/
129 (eg. 'CompileR' gathering the 'CompileI' /class instances/,
130 or the more tricky 'Term' /type-level list-zipper/
131 gathering 'Sym_of_Iface' /class instances/
132 while providing in scope the current 'Sym_of_Iface'
133 within each 'Term' built in a 'CompileI' /class instance/).
134 .
135 __Main extensions__
136 .
137 * @GADTs@ for knowing types by pattern-matching terms,
138 or building terms by using type classes.
139 * @Rank2Types@ for parsing @GADT@s.
140 * @TypeInType@ (introduced in GHC 8.0.1)
141 for 'Type' to also bind a kind equality for the type @h@ it encodes.
142 Which makes the /type application/ (':$')
143 give us an /arrow kind/ for the Haskell /type constructor/
144 it applies an Haskell type to, releaving me from tricky workarounds.
145 * @ConstraintKinds@ for @cs@ to contain 'Constraint's,
146 or defining /type synonym/ of /type classes/,
147 or merging /type constraints/.
148 * @DataKinds@ for type-level data structures (eg. /type-level lists/).
149 * @TypeFamilies@ for type-level programming.
150 * @UndecidableInstances@ for type-level programming
151 that may never terminate.
152 * @PolyKinds@ for avoiding a lot of uses of 'Proxy'.
153 * @TypeApplications@ for having a more concise syntax
154 to build 'Type' (eg. @ty \@Bool@).
155 * @DefaultSignatures@ for providing identity transformations of terms,
156 and thus avoid boilerplate code when a transformation
157 does not need to alter all semantics.
158 As explained in <https://ro-che.info/articles/2016-02-03-finally-tagless-boilerplate Reducing boilerplate in finally tagless style>.
159 .
160 __Bugs__
161 .
162 There are some of them hidding in there,
163 and the whole thing is far from being perfect!
164 Whatever your comments, problem reports, or questions, they are welcome!
165 You have my email address, so… just send me some emails :]
166 .
167 __To do__
168 .
169 * Study to which point /type inferencing/ is doable,
170 now that 'Type' is powerful enough to handle 'TyVar's.
171 * Study to which point error messages can be improved,
172 now that there is a 'Source' carried through all 'Kind's or 'Type's,
173 it should enable some nice reports.
174 * A lot of common terms should be added in @Lib.*@ modules.
175 * No transformation is implemented so far,
176 maybe there should be some, at least as examples
177 to demonstrate their power.
178 * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas.
179 extra-source-files:
180 extra-tmp-files:
181 -- homepage:
182 license: GPL-3
183 license-file: COPYING
184 maintainer: Julien Moutinho <julm+symantic@autogeree.net>
185 name: symantic
186 stability: experimental
187 synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL
188 tested-with: GHC==8.0.2
189 -- PVP: +-+------- breaking API changes
190 -- | | +----- non-breaking API additions
191 -- | | | +--- code changes with no API change
192 version: 5.0.0.20170430
193
194 Source-Repository head
195 location: git://git.autogeree.net/symantic
196 type: git
197
198 Library
199 default-extensions:
200 DataKinds
201 DefaultSignatures
202 FlexibleContexts
203 FlexibleInstances
204 InstanceSigs
205 LambdaCase
206 MultiParamTypeClasses
207 NamedFieldPuns
208 OverloadedStrings
209 Rank2Types
210 ScopedTypeVariables
211 StandaloneDeriving
212 TupleSections
213 TypeApplications
214 TypeFamilies
215 TypeOperators
216 ghc-options: -Wall
217 -fwarn-incomplete-patterns
218 -fno-warn-tabs
219 -fprint-explicit-kinds
220 default-language: Haskell2010
221 exposed-modules:
222 Language.Symantic
223 -- Language.Symantic.Compiling
224 -- Language.Symantic.Compiling.Term
225 -- Language.Symantic.Compiling.Term.Grammar
226 Language.Symantic.Helper.Data.Type.List
227 Language.Symantic.Helper.Data.Type.Peano
228 Language.Symantic.Interpreting
229 Language.Symantic.Interpreting.Dup
230 Language.Symantic.Interpreting.Host
231 Language.Symantic.Interpreting.Text
232 Language.Symantic.Parsing
233 Language.Symantic.Parsing.Token
234 Language.Symantic.Transforming
235 Language.Symantic.Transforming.Trans
236 Language.Symantic.Typing
237 Language.Symantic.Typing.Constant
238 Language.Symantic.Typing.Constraint
239 Language.Symantic.Typing.Family
240 Language.Symantic.Typing.Kind
241 Language.Symantic.Typing.Type
242 build-depends:
243 base >= 4.6 && < 5
244 , containers
245 , ghc-prim
246 , mono-traversable
247 , symantic-grammar
248 , transformers
249 , text