unfortunately no, Idris's dependent types do not subsume type families.
Haskell's type families let you write a type level function that takes a type and it lets you pattern match on what that type is, while Idris doesn't let typecase:https://stackoverflow.com/questions/23220884/why-is-typecase-a-bad-thing …
-
-
Replying to @cattheory
Huh, that’s too bad. I should read the type family paper(s) then. Thanks for sharing!
1 reply 0 retweets 0 likes -
Replying to @mx00s @cattheory
Do you know of any languages besides Haskell that currently support this?
1 reply 0 retweets 0 likes -
Replying to @mx00s @mekajfire
joomy Retweeted Vilem might have
I don't, but
@buggymcbugfix mentioned recently that typecase might make it into Idris 2!https://twitter.com/buggymcbugfix/status/1084975946518708224 …joomy added,
1 reply 0 retweets 2 likes -
My understanding is that Idris 2 is based on quantitative type theory which lets you add "multiplicities" before argument binders: 0, 1 or many. It means you can use that argument that many times in the definition. Using 0 before a type arg would mean you'd have parametricity!
1 reply 0 retweets 2 likes -
-
I guess
@buggymcbugfix's reasoning (unless he has insider info) is that if 0 suffices to express that, then why not have typecase? (he can correct me if I'm wrong) You can find the implementation notes of Idris 2 here: https://github.com/edwinb/Blodwen/blob/master/Notes/implementation-notes.md …2 replies 0 retweets 4 likes -
Replying to @cattheory @mekajfire
Yup, that's the reasoning. I recall discussing this with
@edwinbrady when he came over to@UniKentComp a few weeks ago. Correct me if I'm wrong, Edwin. I also discussed this with Andreas Abel at POPL and he seemed excited about this too.1 reply 0 retweets 5 likes -
Replying to @buggymcbugfix @cattheory and
Yes, that sounds about right! I haven't tried it yet though.
1 reply 0 retweets 4 likes -
Replying to @edwinbrady @buggymcbugfix and
Sage Retweeted Edwin Brady
That was quick work! Thank you,
@edwinbrady :)https://twitter.com/edwinbrady/status/1088811837376876545 …Sage added,
1 reply 0 retweets 2 likes
It was this thread that made me think it was a good way to procrastinate today :). It doesn't work with function types yet, however.
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.