So far doing things in Idris seems like "If you want to write an application, you must first invent the universe"...
-
-
Replying to @ReinH @edwinbrady
This is really cool for learning but not quite as cool for Getting Things Done.
1 reply 0 retweets 1 like -
Replying to @ReinH
That is a fair comment! The book aims more at fundamentals of TypeDD, because that is more useful in the long run.
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
Yes, not a comment on the book per se, just on the state of the ecosystem... which in any event is natural for a young language.
1 reply 0 retweets 0 likes -
Replying to @ReinH
I think we have lots to learn about how best to use dependent types as well. It’s fun finding out.
2 replies 0 retweets 4 likes -
Replying to @edwinbrady
Yeah, my questions now are like "Ok, he's how I can port this from Haskell, but what would be idiomatic use of dependent types?"
2 replies 0 retweets 1 like -
Replying to @ReinH @edwinbrady
Sometimes I feel like I couldn't have come up with the solutions I find, which can be a bit intimidating.
2 replies 0 retweets 0 likes -
Replying to @ReinH @edwinbrady
The tradeoffs around safety, correctness, ease of use, ergonomics are very different despite the superficial similarity to Haskell.
1 reply 1 retweet 0 likes -
Replying to @ReinH
Right. The sweet spot is hard to find - I tend to start by aiming at totality (and no more). It’s easy to get carried away otherwise.
1 reply 3 retweets 4 likes -
Replying to @edwinbrady
In Haskell, the power to weight ratio of dependent types is so poor that they seem like overkill in almost every situation.
2 replies 0 retweets 1 like
That’s my feeling too. I don’t use them in Haskell because I tend to write myself into a hole… writing Idris in Haskell is also bad…
-
-
Replying to @edwinbrady
One thing I'm interested in is the adjunction between length : List a -> n and Vect n a, what other adjunctions exist for other structures?
1 reply 0 retweets 0 likes -
Replying to @ReinH @edwinbrady
Reading
@pigworker's tps://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf was a revelation.0 replies 0 retweets 1 like
End of conversation
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.