Skip to content

Instantly share code, notes, and snippets.

View plaidfinch's full-sized avatar

plaidfinch plaidfinch

View GitHub Profile
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Fixes where
@plaidfinch
plaidfinch / Continuations.hs
Last active February 28, 2018 17:27
Playing around with explicit CPS in Haskell
{-# language ScopedTypeVariables, LambdaCase, TypeApplications #-}
module Continuations where
import Data.String
import Control.Monad
-- Short-circuiting evaluation

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
plaidfinch / Ding.el
Last active August 5, 2016 06:56
Configure flycheck to make a "ding!" sound after it completes checking, only in certain modes
;; 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
plaidfinch / pretty-pragmata.el
Last active July 15, 2021 01:56
Mappings for prettify-symbols-mode to enable Pragmata Pro's ligatures in Emacs. I've taken some slight liberties with the original ligature map, to suit my own tastes.
;; PRETTIFY SYMBOLS (with Pragmata Pro)
(defun setup-pragmata-ligatures ()
(setq prettify-symbols-alist
(append prettify-symbols-alist
'(("!!" . ?)
("!=" . ?)
("!==" . ?)
("!≡" . ?)
("!≡≡" . ?)
("!>" . ?)
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
module TeachingGADTs where
@plaidfinch
plaidfinch / Cooperational.hs
Created February 7, 2015 22:20
The Coöperational Comonad
{-# LANGUAGE GADTs #-}
module Cooperational where
import Control.Monad
import Control.Applicative
import Control.Comonad
data Oper f a =
Return a
@plaidfinch
plaidfinch / Spiral.hs
Created February 5, 2015 05:18
The `spiral` function: a perplexing piece of coinduction
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
plaidfinch / SOP.hs
Last active August 29, 2015 14:12
Playing with sums of products
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
@plaidfinch
plaidfinch / FunWithDictionaries.hs
Last active August 29, 2015 14:12
Playing with Data.Constraint for great fun
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Constraint
import Data.Proxy