@edwinbrady Hey, been getting into Idris more since your book and it's great. Is there any progress on a package manager btw? Can I help?
-
-
Replying to @ReinH @edwinbrady
So far doing things in Idris seems like "If you want to write an application, you must first invent the universe"...
1 reply 0 retweets 3 likes -
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
Hmm, what sort of thing do you mean? There might be (probably are) things we’re not explaining very well.
-
-
Replying to @edwinbrady
There are some applications of dependent types that are intuitive to me, like indexed monads. I still don't grok the full possibilities.
0 replies 0 retweets 0 likesThanks. Twitter will use this to make your timeline better. UndoUndo
-
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.