@edwinbrady still bothering (even if ur busy in conf) Any comment on possibility or stupidity of this in Idris? https://gist.github.com/mandubian/41711e13a7ce3805da4499060141c947 …
-
-
Replying to @mandubian
it looks like it ought to work. When I get near a computer I'll try it...
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
Thks :) I've tried many things searching Idris code for sample but haven't found an "idiomatic" way that would work as I expect
2 replies 0 retweets 0 likes -
Replying to @mandubian @edwinbrady
It may interest you:https://github.com/berewt/UnionType …
1 reply 0 retweets 0 likes -
Replying to @BeRewt
thks... same topic but my main issue is the type alias, not the type itself ;) CC
@edwinbrady2 replies 0 retweets 0 likes -
Replying to @mandubian @edwinbrady
First: add an infix declaration of the (:+:) operator before its definition.
1 reply 0 retweets 0 likes -
-
Replying to @mandubian @edwinbrady
oops, sorry... So, I'm stick with the same "No explicit types on lhs" then now I guess. ;)
1 reply 0 retweets 0 likes -
Replying to @BeRewt @mandubian
I can’t immediately work out a way to express this…
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
no problem... that idea of type aliasing with a type function seemed quite natural & useful case to me...
@BeRewt1 reply 0 retweets 0 likes
It would be nice to allow this sort of thing.
-
-
Replying to @edwinbrady
completely agree... in this case, you don't mix values & types in function but just manipulate types to build types
@BeRewt1 reply 0 retweets 0 likes -
Replying to @mandubian @edwinbrady
so it's not touched by type erasure yet...
@BeRewt1 reply 0 retweets 0 likes - 3 more replies
New conversation -
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.