david-christiansen

Keybase proof

I hereby claim:

• I am david-christiansen on github.
• I am d_christiansen (https://keybase.io/d_christiansen) on keybase.
• I have a public key whose fingerprint is 2709 89EB 2214 50FA DD57 54A8 34B5 BFDB 0942 94C3

To claim this, I am signing this object:

david-christiansen

package dep

import scala.language._

object Dep extends App {

  sealed trait Nat {
    type Plus[M <: Nat] <: Nat
    def plus[M <: Nat](m: M): Plus[M]
  }

david-christiansen

(defun helm-ghc-errors-in-buffer ()
  (with-current-buffer helm-current-buffer
    (remove-if-not #'(lambda (o) (overlay-get o 'ghc-check))
                   (overlays-in (point-min) (point-max)))))

(defun helm-ghc-describe-overlay (o)
  (cl-flet ((abbreviate (str)
                        (if (> (length str) fill-column)
                            (concat (substring str 0 (- fill-column 3)) "...")

david-christiansen

;;; Helm support for finding my stuff
(defvar helm-david-christiansen-git-repo-list nil
  "The Git repos found for my Helm launcher.")
(defvar helm-david-christiansen-git-repo-finder-process nil
  "The process finding Git repos for my Helm launcher.")
(defun helm-david-christiansen-git-repo-finder-output-filter (proc string)
  (when (buffer-live-p (process-buffer proc))
    (with-current-buffer (process-buffer proc)
      (let ((moving (= (point) (process-mark proc))))
        (save-excursion

david-christiansen

module Snoc

data SnocList : List a -> Type where
  SnocNil : SnocList []
  Snoc : (xs : List a) -> (x : a) -> SnocList (xs ++ [x])

snocList : (xs : List a) -> SnocList xs
snocList [] = SnocNil
snocList (x :: xs) with (snocList xs)
  snocList (x :: []) | SnocNil = Snoc [] x

david-christiansen

module VeryFun

class VeryFun (f : Type -> Type) (dict : Functor f) | f where
  funIdentity : {a : Type} -> (x : f a) ->
                map @{dict} id x = id x
  funComposition : {a : Type} -> {b : Type} ->
                   (x : f a) -> (g1 : a -> b) -> (g2 : b -> c) ->
                   map @{dict} (g2 . g1) x = (map @{dict} g2 . map @{dict} g1) x

instance VeryFun List %instance where

david-christiansen

module Finite

import Data.Fin
import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

||| A bijection between some type and bounded numbers
data Finite : Type -> Nat -> Type where

david-christiansen

module MkShow

import Language.Reflection.Elab

mkShow : (a : Type) -> (a -> String) -> Show a
mkShow = %runElab (fill (Var (SN (InstanceCtorN `{Show}))) *> solve)

shower : Show Float
shower = mkShow _ (const "oops")

david-christiansen

module MkMonoid

import Language.Reflection.Elab

||| Generate a Monoid dictionary
total
mkMonoid : Semigroup a => (neutral : a) -> Monoid a
mkMonoid @{semigroup} neutral = mkMonoid' _ semigroup neutral
  where
    mkMonoid' : (a : Type) -> (constr : Semigroup a) -> a -> Monoid a

david-christiansen

||| A port of Chung-Kil Hur's Agda proof that type constructor
||| injectivity is incompatible with LEM.
|||
||| See https://lists.chalmers.se/pipermail/agda/2010/001526.html
||| and its follow-ups for a good discussion.
module AntiClassical

%default total

||| Law of the excluded middle, with an appropriately classical name