This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive bin : Type := | |
| Zero : bin | |
| Twice : bin -> bin | |
| TwicePlusOne : bin -> bin. | |
Fixpoint incr (b : bin) : bin := | |
match b with | |
| Zero => TwicePlusOne Zero | |
| Twice b' => TwicePlusOne b' | |
| TwicePlusOne b' => Twice (incr b') |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive nat : Type := | |
| O : nat | |
| S : nat -> nat. | |
Fixpoint beq_nat (n m : nat) : bool := | |
match n with | |
| O => match m with | |
| O => true | |
| S m' => false | |
end |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# Little aliases and tidbits. | |
# Assumes shell is `zsh`. | |
if [ $(uname | tr [A-Z] [a-z]) = "darwin" ]; then | |
time="gtime" # GNU time installed via homebrew | |
fi | |
# Show revision history and full commit on right hand side. | |
commits() { | |
limit_arg=$1 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is code from the tutorial [A Gentle Introduction to Monad Transformers](https://github.com/kqr/gists/blob/master/articles/gentle-introduction-monad-transformers.md) | |
> {-# LANGUAGE OverloadedStrings #-} | |
> | |
> import Data.Text | |
> import Data.Text.IO as T | |
> import Data.Map as Map | |
> import Control.Applicative | |
> | |
> data ExceptT e m a = ExceptT { |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Code from the blog post "Basic Type Level Programming" by Matt Parsons | |
-- http://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html | |
-- | |
-- References https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE FlexibleContexts #-} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Source https://stackoverflow.com/a/13209294/2748415 | |
{-# LANGUAGE DeriveFunctor #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE TypeOperators #-} | |
-- Thud just goes 'Thud'. | |
data Thud a = Thud | |
deriving (Show, Functor) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
const d = x => decodeURIComponent(x); | |
d('http%253A'); | |
// => "http%3A" | |
d(d('http%253A')); | |
// => "http:" |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
type UnionTy = 'a' | 'b'; | |
type Arr = Array<UnionTy | UnionTy[]>; | |
interface Demo { | |
prop: Arr, | |
} | |
const demo: Demo = { | |
prop: ['a', ['a', 'b']] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
'use strict'; | |
var obj0 = { | |
a: { | |
b: 12 | |
} | |
}; | |
var obj1 = Object.assign({}, obj0); // Similar to object spread. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
interface Some<V> { | |
tag: 'Some'; | |
value: V; | |
} | |
// A nullary type, which is just a tag at runtime for our purposes. | |
interface None { | |
tag: 'None'; | |
} |
OlderNewer