justanotherdot

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

justanotherdot

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')

justanotherdot

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 {

justanotherdot

-- 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 #-}

justanotherdot

-- Source https://stackoverflow.com/a/13209294/2748415

{-# LANGUAGE DeriveFunctor     #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators     #-}

-- Thud just goes 'Thud'.
data Thud a = Thud
  deriving (Show, Functor)

justanotherdot

const d = x => decodeURIComponent(x);
d('http%253A');
// => "http%3A"
d(d('http%253A'));
// => "http:"

justanotherdot

type UnionTy = 'a' | 'b';

type Arr = Array<UnionTy | UnionTy[]>;

interface Demo {
  prop: Arr,
}

const demo: Demo = {
  prop: ['a', ['a', 'b']]

justanotherdot

'use strict';

var obj0 = {
  a: {
    b: 12
  }
};

var obj1 = Object.assign({}, obj0); // Similar to object spread.

justanotherdot

interface Some<V> {
  tag: 'Some';
  value: V;
}

// A nullary type, which is just a tag at runtime for our purposes.
interface None {
  tag: 'None';
}

justanotherdot

// Our ideal type.
interface Foo {
    readonly a: number;
}
type Section = Foo[]; 
type Group = Section[]; 

// Now we start messing with TS.

// `extends` and `optional?` allow us to add almost