plaidfinch

{-# LANGUAGE GADTs           #-}
{-# LANGUAGE PolyKinds       #-}
{-# LANGUAGE DataKinds       #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE TypeOperators   #-}

import Data.Constraint
import Data.Proxy

plaidfinch

{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE ScopedTypeVariables    #-}

import Data.Constraint
import Data.Proxy

plaidfinch

{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE FlexibleContexts       #-}

plaidfinch

module Spiral where

-- Based on <pigworker.wordpress.com/2015/01/02/coinduction>

data Tree x = Leaf x
            | Branch x (Tree x) (Tree x)
            deriving ( Show )

data Stream x = x :> Stream x
              deriving ( Show )

plaidfinch

{-# LANGUAGE GADTs #-}

module Cooperational where

import Control.Monad
import Control.Applicative
import Control.Comonad

data Oper f a =
     Return a

plaidfinch

{-# LANGUAGE GADTs               #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE ScopedTypeVariables #-}

module TeachingGADTs where

plaidfinch

  ;; PRETTIFY SYMBOLS (with Pragmata Pro)
  (defun setup-pragmata-ligatures ()
    (setq prettify-symbols-alist
          (append prettify-symbols-alist
           '(("!!"   . ?)
             ("!="   . ?)
             ("!=="  . ?)
             ("!≡"   . ?)
             ("!≡≡"  . ?)
             ("!>"   . ?)

plaidfinch

  ;; Noisy Flycheck (for slow syntax checkers, program verifiers, &c.)
  (defvar flycheck-ding t)                                    ;; Enable sounds?
  (defvar flycheck-ding-path "~/.emacs.d/private/Ding.mp3")   ;; Where's the "ding!" sound to make?
  (defvar flycheck-buzz-path "~/.emacs.d/private/Basso.aiff") ;; Where's the "bzz!" sound to make?
  (defvar flycheck-noisy-modes-list '(dafny-mode))            ;; Which modes should we make sounds in?

  ;; Below what number of seconds checking time should we be silent?
  (defvar flycheck-ding-delay-threshold 2)
  (defvar flycheck-buzz-delay-threshold 1)

plaidfinch

Keybase proof

I hereby claim:

• I am kwf on github.
• I am kwf (https://keybase.io/kwf) on keybase.
• I have a public key whose fingerprint is E6D1 D4C2 5CBE 5A89 741F 6A04 64DB 17E8 EB41 6853

To claim this, I am signing this object:

plaidfinch

{-# language ScopedTypeVariables, LambdaCase, TypeApplications #-}

module Continuations where

import Data.String
import Control.Monad


-- Short-circuiting evaluation