During SPJ’s keynote about linear Haskell today, I started wondering about the relationship between linear and dependent types. It seems like there’s a big overlap in their use cases, and that DTs are strictly more powerful than LTs. Is that correct?
-
-
Replying to @cbirchall
I haven't this depth of knowledge about type theories but I know
@edwinbrady had implemented uniqueness types in Idris which are inspired by linear types http://docs.idris-lang.org/en/latest/reference/uniqueness-types.html … ... maybe he can tell more about your question?2 replies 0 retweets 1 like -
Replying to @mandubian @cbirchall
I did, but it was really just a hack to see what additional power it would give. Many things became a lot easier, but I didn't take it any further due to lack of understanding the theory.
2 replies 0 retweets 1 like -
So, now that
@pigworker and@bentnib have worked out how to combine linear and dependent types, they're on their way... for example: https://github.com/edwinb/Blodwen/blob/master/tests/blodwen/linear002/door.blod …1 reply 0 retweets 4 likes -
Replying to @edwinbrady @mandubian and
I haven't found anything yet that can't be expressed with dependent types, but linear types make things so much easier. And I expect that purity (that is, not even exceptions or partiality) will turn out to be very valuable.
1 reply 0 retweets 2 likes -
Replying to @edwinbrady @cbirchall and
when you say it makes things much easier, is it for this special cases or in general compared to dependent types?
1 reply 0 retweets 0 likes -
Replying to @mandubian @cbirchall and
Keeping track of resource state, in particular, is much easier when you have a type system to do that for you, to say that a value has been used. But it's complementary - I expect there'll be a lot of value in combining dependent and linear types.
1 reply 0 retweets 1 like
This was a lot of effort: http://docs.idris-lang.org/en/latest/st/index.html …. But with linear/dependent types I got something similar working in just a few lines. Nothing written up yet, but I like it when the types do the work so I don't have to!
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.