Ported @edwinbrady's Idris merge sort to Agda. Agda code runs 4x faster and doesn't segfault on long lists.https://gist.github.com/UlfNorell/4325f091c4f4fbcbad2581577a4f2903 …
-
-
.
@edwinbrady Yes, the challenge was implicit on account of not enough characters.#dependentlytypedlanguageshootoutThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
@edwinbrady How does the unchecked version on Idris compare to the checked one?@ulfnorell -
@_m_b_j_ Pretty much the same. From my limited prodding, it's the overhead of the C RTS, which prioritises simplicity not speed@ulfnorell
End of conversation
New conversation -
-
-
@edwinbrady@ulfnorell llvm target then? -
@cyocum LLVM is a good idea, though we'd need to think about garbage collection. There have been efforts in the past in this direction. - 7 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.