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.

@jntrnr

Aug 15, 2018

There may definitely be benefit here, but IME it's a minority that gravitate towards heavy use of macros/templates. You may end up optimising towards a relatively small crowd of developers. Are there non-meta programming examples where DT flourish?

Graydon Hoare

@graydon_pub

Aug 15, 2018

The significant uses I’m aware of all involve the logical reading of the types, deriving and passing ghost proof values to demonstrate system invariants. Which unfortunately quite expands the language design task to proof-assistant engineering, and limits the audience.

Brendan Zabarauskas

@brendanzab

Aug 15, 2018

To me it's something that is a possible future direction, but just having DTs seems more and more an inevitability these days for statically typed languages, if only to keep down the complexity (see the plethora of overlapping GHC extensions).

Brendan Zabarauskas

@brendanzab

Aug 15, 2018

There's no need to advertise yourself as dependently typed. Types as 'things you can just pass around to other things' become the norm.

Graydon Hoare

@graydon_pub

Aug 15, 2018

Hmm I think they’d be an even harder sell *without* a clear motivating pattern of use. People already chastise FP folks for making code needlessly baroque.

Replying to

and

I mean, create a new language, but you don't really need to push the dependent type agenda up front - just say you have an 'expressive type system'. You already have motivating examples because they're in the libraries and example applications. Can expand on the theory later.

3:32 AM · Aug 15, 2018Twitter Web Client

Replying to

and

I think if you have them, the machinery is going to be pretty visible and you might as well own it / advertise it. They’re immensely powerful! Like time-lord, Jean Grey, space-folding over-9000 powerful. Just … not without costs, maybe overkill for that todo-list app.

@jntrnr

Aug 15, 2018

It depends on the approach, I suspect. Even Jean Grey wasn't always Phoenix, to use your metaphor. Looking at ways to bend the curve towards usability may be a way to incorporate dependent types without requiring a large upfront time investment by the library consumers.

Show replies