| module Main where | |
| -- | JSON is an incredibly simple format. Even its lists are untyped. | |
| -- | As with all languages, functional programming encourages us to | |
| -- | make a domain-specific language (or DSL) to capture the "ideas" | |
| -- | of the language, which we can then use to talk about its content. | |
| -- | In this little snippet, we'll build a JSON DSL, transform it into | |
| -- | a recursive structure, and then use that result to generate some |
| {-# LANGUAGE OverloadedStrings #-} | |
| {-# OPTIONS_GHC -Wall #-} | |
| -- Set your font to a monospace font which makes this character the same as the line-height: │ | |
| -- | |
| -- Otherwise, you'll see an ugly gap between connected lines if the | |
| -- line-height of the font is high. | |
| -- | |
| -- Example fonts: | |
| -- |
| {-# LANGUAGE TemplateHaskell #-} | |
| module Lens where | |
| import Control.Lens | |
| import Data.Monoid (First, (<>)) | |
| data FooBar = | |
| Foo (Either Int Bool) | |
| | Bar (Maybe Bool) |
| # Add this file to your /etc/nixos/configuration.nix `imports = [ ... ];` attribute. | |
| # | |
| # After running `nixos-rebuild switch`, `systemctl --user start keybase-gui.service` | |
| # can be used to start the Keybase GUI. | |
| # | |
| # Not sure if it's just my tiling window manager, but there is a bit of wonkiness | |
| # with the tray icon. Other than that it works perfectly (as of 2017/11/22). | |
| { pkgs, ... }: |
This is a term that performs modulo 32 addition on two 32-bit binary numbers efficiently on the abstract algorithm.
On this example, I compute 279739872 + 496122620 = 775862492.
binSize= 32
binZero= (binSize r.a.b.c.(a r) a.b.c.c)
binSucc= (binSize r.x.a.b.c.(x b x.(a (r x)) c) a.a)
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)
binToNat= (binSize r.n.x.(x x.f.(f x) x.f.(add n (f x)) f.0 (r (mul 2 n))) n.x.0 1)
| 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) |
| -- 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 |
| {-# LANGUAGE AllowAmbiguousTypes #-} | |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE DeriveGeneric #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE FunctionalDependencies #-} | |
| {-# LANGUAGE GADTs #-} | |
| {-# LANGUAGE KindSignatures #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE TypeApplications #-} |