Skip to content

Instantly share code, notes, and snippets.

View hrb90's full-sized avatar

Harrison Brown hrb90

View GitHub Profile
@AndrasKovacs
AndrasKovacs / TypeLambdas.hs
Last active September 23, 2019 14:48
Type lambdas and induction with GHC 8.4.2 and singletons
{-# 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
@porglezomp
porglezomp / Leftpad.idr
Last active October 7, 2023 23:25
Taking on Hillel's challenge to formally verify leftpad (https://twitter.com/Hillelogram/status/987432181889994759)
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
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)
@nurpax
nurpax / char-rnn.hs
Last active November 9, 2017 15:50
Some char-rnn generated Haskell based on training with the GHC HEAD source code
-- 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
@i-am-tom
i-am-tom / fanfic.md
Last active April 14, 2018 22:13
The morning of Gary Burgess, 01/09/17

"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.

@VictorTaelin
VictorTaelin / promise_monad.md
Last active March 23, 2024 17:49
async/await is just the do-notation of the Promise monad

async/await is just the do-notation of the Promise monad

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

@jameshfisher
jameshfisher / halting_problem_javascript.md
Last active September 7, 2017 01:04
A proof that the Halting problem is undecidable, using JavaScript and examples

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

@rkirsling
rkirsling / LICENSE
Last active December 23, 2023 12:54
Directed Graph Editor
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: