| {-# language TemplateHaskell, ScopedTypeVariables, RankNTypes, | |
| TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs, | |
| TypeOperators, TypeApplications, AllowAmbiguousTypes, | |
| TypeInType, StandaloneDeriving #-} | |
| import Data.Singletons.TH -- singletons 2.4.1 | |
| import Data.Kind | |
| -- some standard stuff for later examples' sake |
| -- Note: There is a more complete explanation at https://github.com/hwayne/lets-prove-leftpad/tree/master/idris | |
| import Data.Vect | |
| -- `minus` is saturating subtraction, so this works like we want it to | |
| eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k | |
| eq_max n Z = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl | |
| eq_max Z (S _) = Refl | |
| eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl | |
| -- The type here says "the result is" padded to (maximum k n), and is padding plus the original |
| -- buildPatSynDetails, so this is a mempty, even the type | |
| -- we generate the same location here. | |
| hsConDeclDetails _ = pprPanic "tcLHsBindsCtOrigin" (ppr val_val_binds) | |
| -------------------- | |
| zonkForeignCall :: FlexibleInfo -> CoreBind | |
| -> Maybe FreeVars -- True <=> supplied EndBinds | |
| -> RecFlag | |
| -> Cts -> ForeignOpt Id |
"For services to the PureScript Community, Gary Burgess!"
You've done it, Gary. Moore, Lineker, Coleman, and now Burgess. All the work was worth it.
The halls erupted with praise. Children dressed as Space Ghost, teens with "I only get high on
Halogen" t-shirts, a giant banner held aloft with the message, "Tuple @garyb me". Through
the noise of the crowds and Phil's uninterpretable Northern accent, he barely managed to hear
his theme tu-
BZZP. BZZP.
CertSimple just wrote a blog post arguing ES2017's async/await was the best thing to happen with JavaScript. I wholeheartedly agree.
In short, one of the (few?) good things about JavaScript used to be how well it handled asynchronous requests. This was mostly thanks to its Scheme-inherited implementation of functions and closures. That, though, was also one of its worst faults, because it led to the "callback hell", an seemingly unavoidable pattern that made highly asynchronous JS code almost unreadable. Many solutions attempted to solve that, but most failed. Promises almost did it, but failed too. Finally, async/await is here and, combined with Promises, it solves the problem for good. On this post, I'll explain why that is the case and trace a link between promises, async/await, the do-notation and monads.
First, let's illustrate the 3 styles by implementing
Having read a few proofs that the halting problem is undecidable, I found that they were quite inaccessible, or that they glossed over important details. To counter this, I've attempted to re-hash the proof using a familiar language, JavaScript, with numerous examples along the way.
This famous proof tells us that there is no general method to determine whether a program will finish running. To illustrate this, we can consider programs as JavaScript function calls, and ask whether it is possible to write a JavaScript function which will tell us
| Copyright (c) 2013 Ross Kirsling | |
| Permission is hereby granted, free of charge, to any person obtaining | |
| a copy of this software and associated documentation files (the | |
| "Software"), to deal in the Software without restriction, including | |
| without limitation the rights to use, copy, modify, merge, publish, | |
| distribute, sublicense, and/or sell copies of the Software, and to | |
| permit persons to whom the Software is furnished to do so, subject to | |
| the following conditions: |
