Skip to content

Instantly share code, notes, and snippets.

Gabriel439 / unrolled.txt
Created Apr 21, 2020
Example of unrolled recursion in Dhall
View unrolled.txt
⊢ :let List/generate =
List/generate : ∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a
⊢ List/generate 10
λ(a : Type)
→ λ(f : Natural → a)
→ [ f 0, f 1, f 2, f 3, f 4, f 5, f 6, f 7, f 8, f 9 ]
Gabriel439 / api-design.txt
Last active Apr 12, 2020
API design notes
View api-design.txt
* Importance of category theory
* Answers the question: "What is a *timeless* API?"
* What does "timeless" mean?
* Likely to still be relevant years from now
* Likely to be low maintenance (since unlikely to change)
* Less likely to be subject to controversy or discussion ("obvious")
* Examples:
* Everything Haskell's typeclassopedia (except maybe `Foldable`)
* Categories / Monoids
* `(.)` / `id`
Gabriel439 /
Created Feb 5, 2020
Notes for livestream on contributing to open source projects

These are my rough notes when preparing for a Haskell livestream that I thought would be worth sharing. Some things are general comments on contributing to the open source ecosystem whereas other notes are specific to the stream (e.g. Haskell and the streamly package)

How things look from a maintainer's point of view (for highly active projects):

  • Reactive

    As projects become more active the maintainer's "inbox" gets pretty large. A

Gabriel439 / Main.hs
Created Dec 5, 2019
Simple Twitter chat bot
View Main.hs
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
import Data.ByteString (ByteString)
import Data.Default.Class (Default(..))
import GHC.Generics (Generic)
import Network.Connection (ConnectionParams(..))
import Options.Generic (ParseRecord)
Gabriel439 /
Created Nov 15, 2019
Awake Security Haskell Livestream

Awake Security Haskell Livestream


Awake Security will be livestreaming a periodic 1-on-1 teaching session on Twitch. The subject of this session will always be one of our engineers teaching another one of our engineers how to do accomplish a practical task in Haskell while remote attendees watch, comment, and ask questions.

Gabriel439 / foreach.dhall
Created Aug 9, 2019
Example of how the equivalent of `foreach` in Dhall is ``
View foreach.dhall
let Prelude =
let FN = Natural/even
let a = 2
let b = 3
let c = 5
Gabriel439 / take.dhall
Created Jul 1, 2019
Dhall implementation of `take`
View take.dhall
{- This is a bit ugly and inefficient. See this thread for a discussion about
adding a `Natural/subtract` built-in to improve this:
let Natural/predecessor : Natural Natural
= λ(n : Natural)
let result = Natural/fold
(Optional Natural)
Gabriel439 / ackermann.dhall
Last active Apr 26, 2020
Ackermann function in Dhall
View ackermann.dhall
-- Credit to:
let iterate
: (Natural Natural) Natural Natural
= λ(f : Natural Natural)
λ(n : Natural)
Natural/fold (n + 1) Natural f 1
let increment : Natural Natural = λ(n : Natural) n + 1
Gabriel439 / increment.dhall
Created Apr 25, 2019
Example of non-trivial equivalence
View increment.dhall
{- If I remember correctly, one consequence of Gödel's second incompleteness
theorem is that extensional equivalence is not decidable in general for
any programming language that can encode Peano numerals.
The exact case that a programming language fails on may differ from language
to language (depending on how many tricks they add to try to detect
non-trivial equivalences). However, many of them will typically fail to
detect the equivalence between two ways to encode `increment` for Peano
Gabriel439 / tree.dhall
Created Dec 18, 2018
Merry Christmas!
View tree.dhall
let Prelude =
let repeat =
λ(t : Text)
λ(n : Natural)
Prelude.`Text`.concat (Prelude.`List`.replicate n Text t)
let spaces = repeat " "
You can’t perform that action at this time.