Conversation

deech
@deech
Totally sold on the modeling benefits of dependent types. "Simple" sum types fall over very quickly.
Quote Tweet
@edwinb@types.pl
@edwinbrady
·
Replying to @RasmusKallqvist
Sure (I guess you mean "dependent"). The function for getting the variable also requires an implicit proof that it's valid variable for Idris, and to be valid, it has to be in the table with the documentation strings. github.com/idris-lang/Idr
1
30
Anthony Cowley
@a_cowley
Going between Haskell, Rust, and C++ really drives home how helpful simple sum types are. I don't think they fall over at all. I want dependent types, but I'd like to work with something other than a dull club when making do without.
1
16
deech
@deech
I didn't mean to say dep. types or bust. But not granular enough sum types are really hard to back out once the codebase gets big enough especially if a bunch of them get tupled. You can end up with tons of "validated" smart constructed types which are a pain.
2
9
Philippa Cowderoy
@flippac
Our ongoing inability to usefully relate sum types to each other effectively is a huge PITA. We need a better combination of structural and nominal typing than I'm used to seeing! (Compile-time gensym would be nice, too)
3
8
Show replies