Skip to content

Instantly share code, notes, and snippets.

Gabriel Gonzalez Gabriel439

Block or report user

Report or block Gabriel439

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
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, 2019
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 " "
Gabriel439 / package.dhall
Created Apr 7, 2018
The Cabal file format encoded as a Dhall type
View package.dhall
let Version = (Version : Type) (v : Text Version) Version
in let VersionRange =
(VersionRange : Type)
(anyVersion : VersionRange)
(noVersion : VersionRange)
(thisVersion : Version VersionRange)
(notThisVersion : Version VersionRange)
(laterVersion : Version VersionRange)
(earlierVersion : Version VersionRange)
Gabriel439 / fibonacci.hs
Created Mar 25, 2018
Efficient fibonacci numbers using infinite precision integer arithmetic
View fibonacci.hs
import Numeric.Natural (Natural)
import qualified Data.Semigroup
-- | @fibonacci n@ computes the @nth@ fibonacci number efficiently using infinite
-- precision integer arithmetic
-- Try @fibonacci 1000000@
fibonacci :: Natural -> Natural
fibonacci n = x01 (Data.Semigroup.mtimesDefault n m)
Gabriel439 / Main.purs
Last active Mar 31, 2018
Purescript Flare - Simon example
View Main.purs
module Main where
import Data.Array ((..), reverse)
import Data.Int (toNumber)
import Flare (UI, radioGroup)
import Flare.Drawing (runFlareDrawing)
import Graphics.Drawing
import Graphics.Drawing.Font (font, sansSerif, bold)
import Math (cos, sin, pi)
import Prelude
View gist:011424bec6d839d98b0b
import Numeric.AD
assert = print
eval = id
main = do
let a x = 2 * x^2 + 3
let b = eval a 1
assert (b == 5) -- Prints `True`
Gabriel439 / gist:be7c8cfc536be91ef4f5
Last active Aug 29, 2015
Quick annah walkthrough
View gist:be7c8cfc536be91ef4f5
-- Example Annah programs and their reductions
-- I'll start with simple non-recursive data types so that you can get a feel for the syntax and then work up to recursive data
-- types followed by mutually recursive types
-- Example #1: Bool, the type
$ annah
type Bool
data True
data False
in Bool
You can’t perform that action at this time.