author: Julien Moutinho bug-reports: Julien Moutinho build-type: Simple cabal-version: >= 1.24 category: Language description: Library for composing, typing, compiling, transforming and interpreting a custom DSL (Domain-Specific Language) expressing a subset of GHC's Haskell. . __Main ideas__ . * 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/ to encode their /semantics/ (eg. @(Sym_Bool HostI)@ interprets the term as a @Bool@ or @(Sym_Bool TextI)@ interprets the term as a @Text@). /Lambda abstractions/ being handled by an higher-order approach, meaning that it directly reuses 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). * 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 wrapped inside a @Proxy@ to fit into a /type-level list/ (eg. @cs ~ [Proxy Bool, Proxy (->), Proxy Eq]@). * 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@. I guess there is a similarity with (as exploited in for instance), but not knowing much about them I can't tell, I just came up using /type-level lists/ by hacking 's @Elem@, and now have no incentive to study and compare these techniques: /type-level lists/ are simple enough. * 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 be @GADT@-like in the kind of the Haskell 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 us 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 . . __Usage__ . There are a few examples in the @Test.hs@ files, and shall be more one day in the of this library. . __Bugs__ . Your comments, problem reports, or questions are welcome! :-) . __TODO__ . * /Type inferencing/ to improve the current hand written /type checking/, and remove some type annotations in the DSL. Currently all /lambda abstractions/ 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@). * A lot of common terms should be added in @Compiling.*@ modules. Maybe as separate packages to limit dependencies. * No transformation is implemented so far, there should be some, at least as examples to demonstrate their power. 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.1 version: 3.20170104 Source-Repository head location: git://git.autogeree.net/symantic type: git Library default-extensions: DataKinds DefaultSignatures FlexibleContexts FlexibleInstances InstanceSigs MultiParamTypeClasses OverloadedStrings Rank2Types ScopedTypeVariables StandaloneDeriving TypeApplications TypeFamilies TypeOperators ghc-options: -Wall -fno-warn-tabs -fprint-explicit-kinds default-language: Haskell2010 exposed-modules: Language.Symantic Language.Symantic.Compiling Language.Symantic.Compiling.Applicative Language.Symantic.Compiling.Bool Language.Symantic.Compiling.Char Language.Symantic.Compiling.Either Language.Symantic.Compiling.Eq Language.Symantic.Compiling.Foldable Language.Symantic.Compiling.Functor Language.Symantic.Compiling.IO Language.Symantic.Compiling.If Language.Symantic.Compiling.Int Language.Symantic.Compiling.Integer Language.Symantic.Compiling.Integral Language.Symantic.Compiling.List Language.Symantic.Compiling.Map Language.Symantic.Compiling.Maybe Language.Symantic.Compiling.Monad Language.Symantic.Compiling.MonoFoldable Language.Symantic.Compiling.MonoFunctor Language.Symantic.Compiling.Monoid Language.Symantic.Compiling.NonNull Language.Symantic.Compiling.Num Language.Symantic.Compiling.Ord Language.Symantic.Compiling.Sequences Language.Symantic.Compiling.Show Language.Symantic.Compiling.Term Language.Symantic.Compiling.Text Language.Symantic.Compiling.Traversable Language.Symantic.Compiling.Tuple2 Language.Symantic.Compiling.Unit Language.Symantic.Interpreting Language.Symantic.Interpreting.Dup Language.Symantic.Interpreting.Host Language.Symantic.Interpreting.Text Language.Symantic.Lib.Data.Type.List Language.Symantic.Lib.Data.Type.Peano 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 , transformers , text Test-Suite symantic-test type: exitcode-stdio-1.0 default-extensions: DataKinds FlexibleContexts FlexibleInstances MultiParamTypeClasses OverloadedStrings ScopedTypeVariables TupleSections TypeApplications TypeFamilies TypeOperators default-language: Haskell2010 ghc-options: -Wall -fno-warn-tabs -main-is Test -- -fprint-explicit-kinds hs-source-dirs: Language/Symantic main-is: Test.hs other-modules: Compiling.Applicative.Test Compiling.Bool.Test Compiling.Foldable.Test Compiling.Functor.Test Compiling.Map.Test Compiling.MonoFunctor.Test Compiling.Term.Test Compiling.Test Parsing.Test Typing.Test build-depends: base >= 4.6 && < 5 , containers , mono-traversable , transformers , tasty >= 0.11 , tasty-hunit , text , symantic