TOTBWF/tactic-haskell

Implement Extended Type Language

Opened this issue · 1 comments

TOTBWF commented

This has quite a few benefits.

  1. We can have a custom quasi-quoter, which helps us both from an ergonomics and tooling perspective.
    This would enable the syntax: tactic [thm| foo :: a -> b -> (a, b) |] $ do ..., as well as allow us to (potentially) use tactic-haskell as an editor tool.

  2. New types. This would open the door for actual dependent types, which would be a huge win. I'm not sure about the exact specifics of what the desugaring would look like in a few cases, but we could always limit the tricky bits to be only usable within the context of tactics.

TOTBWF commented

Now that I think about it, the only thing that really ties us to template-haskell is reify and friends.
If we take an intero style approach, and use ghci to get our info, we could totally remove template-haskell as a dependency, which would allow us to operate without being stuck in Q. It would probably make sense to keep some ability to use Q directly though, so perhaps using some sort of mtl style api would make the most sense.