Instantly share code, notes, and snippets.

# Gabriel GonzalezGabriel439

• Sort options
Created Aug 9, 2019
Example of how the equivalent of `foreach` in Dhall is `Prelude.List.map`
View foreach.dhall
 let Prelude = https://prelude.dhall-lang.org/package.dhall let FN = Natural/even let a = 2 let b = 3 let c = 5
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: https://github.com/dhall-lang/dhall-lang/issues/602#issuecomment-505484434 -} let Natural/predecessor : Natural → Natural = λ(n : Natural) → let result = Natural/fold n (Optional Natural)
Last active Apr 26, 2019
Ackermann function in Dhall
View ackermann.dhall
 -- Credit to: https://news.ycombinator.com/item?id=15186988 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
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 numerals.
Created Dec 18, 2018
Merry Christmas!
View tree.dhall
 let Prelude = https://prelude.dhall-lang.org/package.dhall sha256:534e4a9e687ba74bfac71b30fc27aa269c0465087ef79bf483e876781602a454 let repeat = λ(t : Text) → λ(n : Natural) → Prelude.`Text`.concat (Prelude.`List`.replicate n Text t) let spaces = repeat " "
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)
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)
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
Created Apr 25, 2015
Good game
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`
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.