author: Julien Moutinho bug-reports: Julien Moutinho build-type: Simple cabal-version: >= 1.24 category: Language description: __Description__ . Library for composing, typing, compiling, transforming and interpreting a custom DSL (Domain-Specific Language) expressing a subset of GHC's Haskell. Its main goal is to enable the runtime handling of terms typed according to some compile-time defined types. The idea being that the more complex logic shall remain coded in Haskell and then this library used to project an interface into a DSL giving runtime users the flexibility to write simpler programs suited to their needs. . Typical use cases: . * Enabling runtime users to enter some Haskell-like expressions without using all the weight and slowness of GHC at runtime (eg. by using ). * Limiting those expressions to be built from well-controlled expressions only. * Run some analyzes/optimizations on those well-controlled expressions. . __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 all but heavily tested and documented, does not have a strong commitment to preserving backward compatibility, and can just die without notice. Its version follows the , so you may want to use upper-bounds in @build-depends@. This said, hope you'll enjoy the tool :) . __Usage__ . Reading the boring @Test.hs@ files of should give you enough examples to understand how to use this library, and reading some of the repetitively boring and painfully repetitive @Lib/*.hs@ files of should give you some templates and the general pattern to let you extend this library with your own symantics. . The @Test.hs@ files use as parser and a default grammar somehow sticking to Haskell's, but staying context-free (so in particular: insensitive to the indentation). This grammar, itself written as a symantic embedded DSL, can be reused to build another one, is not bound to a specific parser, and can produce its EBNF rendition. . __Main ideas__ . * __Symantic DSL__. To encode terms in the way (aka. the /symantic/ way) i.e. to use a /class/ to encode the /syntax/ of terms (eg. 'Sym_Bool') and /class instances/ on a dedicated type to encode their /semantics/ (eg. @(Sym_Bool HostI)@ interprets a term as a value of its type in the host language (Haskell here), or @(Sym_Bool TextI)@ interprets a term as a textual rendition, etc.). DSL are then composed by selecting those symantic /classes/. When using symantics for an embedded DSL those /classes/ are all inferred by GHC from the terms used, provided that the @NoMonomorphismRestriction@ extension 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/ given to 'compile'. Moreover, the terms 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 DeBruijn encoding nor 's monads). * __Singleton for any type__. To typecheck terms using a @(Type cs h)@ @GADT@ which acts as a /singleton type/ for any Haskell type @h@ buildable by composing the /type constants/ @cs@, each one wrapped inside a @Proxy@ to fit into a common /type-level list/ (eg. @cs ~ [Proxy Bool, Proxy (->), Proxy Eq]@). * __Extensible data type__. To inject a type into a /type-level list/ or project a /type-level list/ onto a type, to compose an /extensible data type/ (eg. the 'Token' @GADT@ gathering the 'TokenT' /data instances/, that a parser can build and then give to 'compile'). This type-level programming requires @UndecidableInstances@, but not @OverlappingInstances@. There is a similarity with (see for instance or ). Those also enable to compose a DSL using some machinery based upon (co)free(r) (co)monads and (cata|ana)morphisms. Which library fits best your problem domain and brain is for you to judge :) On that topic, see also: . Here, I just came up using /type-level lists/ by hacking 's @Elem@. * __Extensible class__. To recurse on a /type-level list/ through /class instances/ to compose an /extensible class/ (eg. 'CompileR' gathering the 'CompileI' /class instances/, or the more tricky 'TermO' /type-level list-zipper/ gathering 'Sym_of_Iface' /class instances/ while providing in scope the current 'Sym_of_Iface' within each 'TermO' built in a 'CompileI' /class instance/). . __Main extensions__ . * @GADTs@ for knowing types by pattern-matching terms, or building terms by using type classes. * @Rank2Types@ for parsing @GADT@s. * @TypeInType@ (introduced in GHC 8.0.1) for 'Type' to also bind a kind equality for the type @h@ it encodes. Which makes the /type application/ (':$') give us an /arrow kind/ for the Haskell /type constructor/ it applies an Haskell type to, releaving me from tricky workarounds. * @ConstraintKinds@ for @cs@ to contain 'Constraint's, or defining /type synonym/ of /type classes/, or merging /type constraints/. * @DataKinds@ for type-level data structures (eg. /type-level lists/). * @TypeFamilies@ for type-level programming. * @UndecidableInstances@ for type-level programming that may never terminate. * @PolyKinds@ for avoiding a lot of uses of 'Proxy'. * @TypeApplications@ for having a more concise syntax to build 'Type' (eg. @ty \@Bool@). * @DefaultSignatures@ for providing identity transformations of terms, and thus avoid boilerplate code when a transformation does not need to alter all semantics. As explained in . . __Bugs__ . 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, so that it would improve the current /type checking/, and remove some type annotations in the DSL. Currently each /lambda abstraction/ must have its variable explicitely typed, and terms must be called with enough arguments to typecheck, be it term arguments (for instance @(+) :: Num a => a -> a -> a@ needs at least one term argument to check @Num a@) or type arguments (for instance @return :: Monad m => a -> m a@ needs a type argument to check @Monad m@). * Study to which point error messages can be improved. * A lot of common terms should be added in @Lib.*@ modules. Maybe as separate packages to limit dependencies. * No transformation is implemented so far, maybe there should be some, at least as examples to demonstrate their power. * Study where to put @INLINE@, @INLINEABLE@ or @SPECIALIZE@ pragmas. extra-source-files: extra-tmp-files: -- homepage: license: GPL-3 license-file: COPYING maintainer: Julien Moutinho name: symantic stability: experimental synopsis: Library for Typed Tagless-Final Higher-Order Composable DSL tested-with: GHC==8.0.2 -- PVP: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change version: 4.2.0.20170208 Source-Repository head location: git://git.autogeree.net/symantic type: git Library default-extensions: DataKinds DefaultSignatures FlexibleContexts FlexibleInstances InstanceSigs LambdaCase MultiParamTypeClasses NamedFieldPuns OverloadedStrings Rank2Types ScopedTypeVariables StandaloneDeriving TupleSections TypeApplications TypeFamilies TypeOperators ghc-options: -Wall -fwarn-incomplete-patterns -fno-warn-tabs -fprint-explicit-kinds default-language: Haskell2010 exposed-modules: Language.Symantic Language.Symantic.Compiling Language.Symantic.Compiling.Term Language.Symantic.Compiling.Term.Grammar Language.Symantic.Helper.Data.Type.List Language.Symantic.Helper.Data.Type.Peano Language.Symantic.Interpreting Language.Symantic.Interpreting.Dup Language.Symantic.Interpreting.Host Language.Symantic.Interpreting.Text Language.Symantic.Parsing Language.Symantic.Parsing.Token Language.Symantic.Transforming Language.Symantic.Transforming.Trans Language.Symantic.Typing Language.Symantic.Typing.Constant Language.Symantic.Typing.Constraint Language.Symantic.Typing.Family Language.Symantic.Typing.Kind Language.Symantic.Typing.Type build-depends: base >= 4.6 && < 5 , containers , ghc-prim , mono-traversable , symantic-grammar , transformers , text