Discussion: Craft a Roadmap? about klister HOT 15 OPEN

demonstrate a "Wow" program
[...]
foo = take 2 . map (+2) $ [1..]
[...]
For klister, this seems to be implementing type classes as a library?

The Haskell example is much smaller than the typeclasses example!

For a small example, what do you think of the megaconst example from our TyDe2020 extended abstract?

from klister.

I think its a good example but is only suited for a small audience. What I would want is the megaconst example complete with a DSL that ties the whole picture together.

So the narrative would be:

• We have this cool language with this cool feature
• Typically one would define a DSL like this: <classic-DSL-example>
• This DSL leverages the host language's type system, but notice that in <classic-DSL-example> we must <do-something-manual>.
• We must <do-something-manual> because the host language is does not use the type at the expansion site to ....blah.
• But with our language this DSL becomes: <DSL-example>
• Notice that <do-something-manual> is missing because <cool-feature>.

surely too long for an abstract, but thats ok this would be the intro example. The point is to first start with a well known DSL for anything, because that is where the audience is, then show how it can better leverage klister's features for some benefit.

from klister.

I think we should have some high level goals and then dispatch tickets in pursuit of these goals.

It's a side-project, you should work on whichever features you are the most passionate about, not the features the rest of us are the most passionate about :)

My personal roadmap for Klister (that is, which features I would work on if I had more time) is:

1. #202
2. #186
3. #184
4. #105
5. #168
6. #167
7. #165
8. #54
9. #119

from klister.

From your list of priorities, the section which speaks to me the most is "Make Klister more usable". I would love to be able to use Klister to solve Advent of Code problems, for example. That's something the Unison team did last year and I think it's a great way to demonstrate the language in a few small bites.

from klister.

absolutely! This is high on my list as well and I think it would help with #202 because we could show the repl examples. That is exactly what I'm after and something like AoC is a great proving ground for programming-in-the-small

from klister.

The point is to first start with a well known DSL for anything, because that is where the audience is, then show how it can better leverage klister's features for some benefit.

I like this idea! Let's see, what are some well-known DSLs...

1. Hutton's Razor (integers and addition)
2. Untyped lambda calculus
3. Simply-typed lambda calculus with type annotation on the lambda parameters
4. Simply-typed lambda calculus with type inference
5. System F
6. Linear lambda calculus
7. π-calculus
8. Session types
9. List comprehension
10. SQL
11. Persistent's model files
12. Diagram languages, like dot or mermaid
13. Servant's type level route descriptions
14. Yesod's "Shakespearean Templates"
15. CSS selectors
16. jq, awk, sed
17. Template engines like Mustache
18. Chess notation

It's a rather heterogeneous list, so I'm sure there are more well-known DSLs from domains I'm not thinking about!

from klister.

there is also:

• lava (circuit description language)
• conal elliot's graphics dsl
• the vim keybinds (although vim doesn't say that's a DSL it is and a program is a key sequence)

from klister.

but anything that should be typed is a prime example.

from klister.

Here's my personal roadmap, if I had any time at all for this. It would be the following series of submissions to various PL conferences:

• Parallel Macro Expansion, a paper on how to use LVar-inspired techniques to get deterministic parallel macro expansion. The key is that macros need side effects to communicate, so those effects need to be reorderable, and things like threshold reads do that.
• Typed Parallel Macro Expansion, gluing Hindley-Milner on top of the last one (basically Klister today plus some inter-macro communication)
• A Refined Semantics for Local Macro Expansion, which would add local-expand to the last one. It would avoid the N^2 overhead of recursive uses of local-expand in Racket by representing the result of local expansion as an opaque object that is evidence for some judgment in the core language, rather than syntax objects. These objects could be processed using an API based on the Edinburgh LCF approach, and using one in a new context would require only a weakening check, which in many useful cases would be only a pointer equality check.
• Time and interest permitting, build an implementation of observational type theory using Klister techniques, with lots of the cool datatype encoding stuff from Pierre-Evariste Dagand's thesis.

from klister.

It's a rather heterogeneous list, so I'm sure there are more well-known DSLs from domains I'm not thinking about!

Chat GPT to the rescue, I asked it to list DSLs with relatively unusual type systems, for example the lambda calculus, and here's the list it gave:

1. Dependent type systems: Coq, Agda, Idris.
2. Session types: Scribble, pi calculus. (I had never heard of Scribble, nice!)
3. Refinement types: Liquid Haskell, F*.
4. Gradual types: TypeScript, Racket.
5. Linear types: linear lambda calculus, Rust.
6. Intersection types: TypeScript, Scala.
7. Polymorphic types: Haskell, ML.
8. Nominal types: Java, C# (and by extension, Structural types: PureScript, go).
9. (Row types: PureScript)

It is relatively easy to implement an intrinsically-typed lambda calculus DSL in Haskell, because the simply-typed lambda calculus is part of Haskell's type system, but it would be harder to implement a calculi with one of those more exotic or more powerful type systems. The problem is that it would also be harder with Klister! The selling point is that our macros can use the types computed by Klister's builtin type system, not that it can be used to define custom type systems, so it's not obvious that Klister would be a better fit.

That being said, implementing type classes in the language is definitely an example of a custom extension to the type system, and I think my implementation of Scala-style implicits counts, so I am hopeful that Klister can be used to define exotic type systems, I just don't have a very good justification for that belief nor a good understanding of the set of type systems which would be easy or hard to implement.

Maybe we should just try implementing a few calculi and see if any of them are easier than expected? Or maybe my Scala-style implicits is already a good example of a "Wow" program? I specifically picked that example because the type system allows the programmer to write less code, as opposed to catch more errors, so it's a good way to illustrate the benefit of type-driven macros.

from klister.

The selling point is that our macros can use the types computed by Klister's builtin type system, not that it can be used to define custom type systems, so it's not obvious that Klister would be a better fit.

So this means Hindley-Milner right? So the "wow" would be a deduction of some type that the audience would normally expect to provide but is given by the HM unification algorithm. Perhaps we could demonstrate a DSL that usually has a rather poor type system like SQL and then show how we get HM "for free" via the embedding in klister as a host language. Another one that might be cool is an array language like J, APL, or BQN. These languages are typically dynamically typed, but I just wonder what an embedding (and a typed one at that) would look like. In any case, the extended abstract does say:

Finally, we hope to explore richer type systems than HindleyMilner, beginning with extensions to higher-kinded polymorphism

So perhaps this list is a good demo list once the project is in a place where richer type systems can be added.

from klister.

Didn't I get higher-kinded polymorphism working? I know there's kind metas in the expander...

from klister.

Didn't I get higher-kinded polymorphism working? I know there's kind metas in the expander...

We have kind inference, but instead of generalizing kind variables like PolyKinds, we default to * like NoPolyKinds.

#92

from klister.

So this means Hindley-Milner right? So the "wow" would be a deduction of some type that the audience would normally expect to provide but is given by the HM unification algorithm.

Hmm, bit Hindley-Milner is very standard, so if HM gives a type, then the audience will expect not to have to write a type signature!

from klister.

Perhaps we could demonstrate a DSL that usually has a rather poor type system like SQL and then show how we get HM "for free" via the embedding in klister as a host language. Another one that might be cool is an array language like J, APL, or BQN.

I don't think that's the right kind of demo either. If I implement a stack language using an intrinsically-typed approach in Haskell, I also get type-checking for free, no need to type-aware macros:

data Expr (before :: [*]) (after :: [*]) where
  IntLit :: Int -> Expr xs (Int ': xs)
  Add :: Expr (Int ': Int ': xs) (Int ': xs)

SQL is a much bigger language, but the same approach works.

from klister.