Conversation

This Tweet is from a suspended account. Learn more

Aug 15, 2018

Not sure if this rhetorical, but I'd be happy to chat strategy. I suspect your best bet would be to a tool that shows the value of dependent types quickly. What is the biggest benefit in having them, and how does the tool/lang show that. Lots to explore from there.

Brendan Zabarauskas

@brendanzab

Aug 15, 2018

I think lots of the initial value will come in type-directed meta programming. Lots of examples from Haskell and Rust and C++ that seem awkward and hacky are nice and beautiful with DTs.

Tom Schouten

@tom_zwizwa

Aug 15, 2018

Brendan, can you give an example of how DT helps meta programming, contrasted to Haskell?

Brendan Zabarauskas

@brendanzab

Aug 16, 2018

Haskell has a lot of good extensions already for doing type-directed code generation, like type class induction, type families, generics, and GADTs, type level literals, etc.

Replying to

This allows you to build cool libraries, like Servant, Bound, and database libraries. Unfortunately all those features feel disjointed (due to them being added on later), contributing to a steep learning curve, making it hard for most programmers to use these features themselves.

4:01 AM · Aug 16, 2018Twitter Web Client

Replying to

An interesting insight is that many of these facilities can be greatly simplified by moving to dependent types. This allows you to use regular old functions at the type level, instead of having a separate type language with slightly different syntax and semantics.

Brendan Zabarauskas

@brendanzab

Aug 16, 2018

I'm probably not being very precise here, and glossing over a bunch of stuff, but that's the general idea at least. There's been good work being done in bringing DTs to Haskell, and hopefully it will simplify things there. But it's a challenging thing to retrofit.

Show replies