文件列表:

CHANGELOG.md (108, 2020-09-15)
LICENSE (1528, 2020-09-15)
Setup.hs (46, 2020-09-15)
cabal.project (164, 2020-09-15)
pilot.cabal (1965, 2020-09-15)
src (0, 2020-09-15)
src\Language (0, 2020-09-15)
src\Language\Pilot.hs (4954, 2020-09-15)
src\Language\Pilot (0, 2020-09-15)
src\Language\Pilot\Examples.hs (9371, 2020-09-15)
src\Language\Pilot\Examples (0, 2020-09-15)
src\Language\Pilot\Examples\Copilot.hs (668, 2020-09-15)
src\Language\Pilot\Examples\Copilot (0, 2020-09-15)
src\Language\Pilot\Examples\Copilot\Clock.hs (2995, 2020-09-15)
src\Language\Pilot\Examples\Copilot\Counter.hs (2878, 2020-09-15)
src\Language\Pilot\Examples\Copilot\Engine.hs (3161, 2020-09-15)
src\Language\Pilot\Examples\Copilot\Heater.hs (2827, 2020-09-15)
src\Language\Pilot\Examples\Copilot\LTL.hs (6064, 2020-09-15)
src\Language\Pilot\Examples\Copilot\Voting.hs (11640, 2020-09-15)
src\Language\Pilot\Interp (0, 2020-09-15)
src\Language\Pilot\Interp\C.hs (187476, 2020-09-15)
src\Language\Pilot\Interp\C (0, 2020-09-15)
src\Language\Pilot\Interp\C\Util.hs (20115, 2020-09-15)
src\Language\Pilot\Interp\Pure.hs (24902, 2020-09-15)
src\Language\Pilot\Interp\Pure (0, 2020-09-15)
src\Language\Pilot\Interp\Pure\Point.hs (10130, 2020-09-15)
src\Language\Pilot\Interp\Pure\PrefixList.hs (5981, 2020-09-15)
src\Language\Pilot\Meta.hs (4745, 2020-09-15)
src\Language\Pilot\Nominal.hs (1995, 2020-09-15)
src\Language\Pilot\Object.hs (39314, 2020-09-15)
src\Language\Pilot\Object (0, 2020-09-15)
src\Language\Pilot\Object\Point.hs (12146, 2020-09-15)
src\Language\Pilot\Repr.hs (8942, 2020-09-15)
src\Language\Pilot\Types.hs (973, 2020-09-15)
src\Language\Pilot\Types (0, 2020-09-15)
src\Language\Pilot\Types\Logic.hs (2428, 2020-09-15)
src\Language\Pilot\Types\Nat.hs (7342, 2020-09-15)
src\Language\Pilot\Types\Represented.hs (1664, 2020-09-15)
... ...

# pilot: C EDSL inspired by copilot ## Why? This is like [copilot](https://github.com/Copilot-Language/copilot) but way more complex from the user's perspecitve. Why does it exist? Because copilot is really cool, but 1. It doesn't support algebraic datatypes; control flow quickly becomes unwieldly since it all must go by way of numbers as it would in C itself 2. It only supports in-Haskell simulation _on paper_; it's inadequate for everything but the most trivial examples 3. All triggers are independent; it is impossible to express sharing between them, which can be problematic in larger deployments 4. Stream prefix sizes are not present at the type level; the notions of `drop` and `(++)` are not typed, and in my experience this is quite error-prone This project aims to fill in these gaps, and also to explore one further idea. Programming in copilot is programming with streams. Familiar notions like arithmetic and bitwise operations are implicitly "lifted" pointwise over streams, and any "point" or "scalar" value can be made into a stream by way of the `constant` function. This is all annoyingly reminiscent of an applicative functor; it's the [ZipList](https://hackage.haskell.org/package/base-4.14.0.0/docs/Control-Applicative.html#t:ZipList), in particular. But within the copilot language itself, there are no functors or applicatives. There aren't even any _functions_ in the language--and we don't _want_ functions in the language--so how could we possibly have functors? The question, then, is whether it is possible to have, within an EDSL that does not even have functions, a programming style similar to that of Haskell's `Functor` and `Applicative`? This project says "Yes!". Read on to find out how. ## Overview The pilot EDSL is expressed in what is essentially the ["tagless-final" style](http://okmij.org/ftp/tagless-final/index.html), except that there's a GADT defining the forms, instead of a bunch of typeclass methods. In the tagless-final style, there's a representation type, which is made to be an instance of the typeclass which gives the abstract forms. In pilot, this representation is split into two parts, and Haskell's products, functions, and terminal object are added into it. ```Haskell -- Language.Pilot.Repr import Language.Pilot.Meta as Meta (Type, Terminal, Obj, type (:->), type (:*)) newtype Repr (f :: Hask -> Hask) (val :: domain -> Hask) (t :: Meta.Type domain) = Repr { getRepr :: f (Val f val t) } data Val (f :: Hask -> Hask) (val :: domain -> Hask) (t :: Meta.Type domain) where Object :: val t -> Val f val (Obj t) Arrow :: (Repr f val s -> Repr f val t) -> Val f val (s :-> t) Product :: (Repr f val s , Repr f val t) -> Val f val (s :* t) Terminal :: Val f val Terminal ``` The tagless-final style typeclass therefore looks like this: ```Haskell -- Language.Pilot.Repr type Interpret (form :: Meta.Type domain -> Hask) f val = forall (x :: Meta.Type domain) . -- The `Rep` is a value-level representation of the type x. -- The `form` is a GADT constructor which represents the abstract form; it -- can use meta-language functions and products, as well as object-language -- types. Rep (Meta.Type domain) x -> form x -> Repr f val x class Monad f => Interprets (form :: Meta.Type domain -> Hask) (f :: Hask -> Hask) (val :: domain -> Hask) where interp :: Interpret form f val ``` Why include meta-language functions, products, and terminal object in the EDSL? Because if we have these things available, then we're able to talk about applicative functors, even in an object-language which does not have functions. Also, these are the ingredients of a [Cartesian closed category](https://en.wikipedia.org/wiki/Cartesian_closed_category), but enough about that.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：