Skip to content

Instantly share code, notes, and snippets.

Avatar

David Thrane Christiansen david-christiansen

View GitHub Profile
@david-christiansen
david-christiansen / Dep.scala
Created Aug 20, 2014
Simple presentation of singletons in Scala
View Dep.scala
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]
}
View anticlassical.idr
||| 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
View keybase.md

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:

View Monoid.idr
import Language.Reflection.Elab
namespace Tactics
||| Restrict a polymorphic type to () for contexts where it doesn't
||| matter. This is nice for sticking `debug` in a context where
||| Idris can't solve the type.
simple : {m : Type -> Type} -> m () -> m ()
simple x = x
@david-christiansen
david-christiansen / FizzBuzzC.idr
Last active Jan 25, 2018
Dependently typed FizzBuzz, now with 30% more constructive thinking
View FizzBuzzC.idr
module FizzBuzzC
%default total
-- Dependently typed FizzBuzz, constructively
-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
ZeroFizzy : Fizzy 0
Fizz : Fizzy n -> Fizzy (3 + n)
@david-christiansen
david-christiansen / JSON.idr
Created Dec 10, 2013
Zygote of a JSON parser
View JSON.idr
module JSON
import Data.HVect
import Control.Monad.Identity
import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Strings
@david-christiansen
david-christiansen / NatInd.idr
Last active Oct 26, 2017
Simple proof automation with reflected elaboration
View NatInd.idr
module NatInd
import Language.Reflection.Elab
import Language.Reflection.Utils
%default total
trivial : Elab ()
trivial = do compute
g <- snd <$> getGoal
@david-christiansen
david-christiansen / PreorderReasoning.idr
Created Dec 14, 2013
Agda-style preorder reasoning in Idris
View PreorderReasoning.idr
module PreOrderReasoning
-- QED is first to get the precedence to work out. It's just refl with an explicit argument.
syntax [expr] "QED" = qed expr
-- foo ={ prf }= bar ={ prf' }= fnord QED
-- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'
syntax [from] "={" [prf] "}=" [to] = step from prf to
--These are the components for using the syntax with equality
@david-christiansen
david-christiansen / ErrorTest.idr
Created Jan 10, 2014
First-ever Idris DSL with domain-specific error messages!
View ErrorTest.idr
module ErrorTest
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
data Ty = TUnit | TFun Ty Ty
@david-christiansen
david-christiansen / ErrorReflectionDemo.idr
Created May 1, 2014
Error reflection demo from today
View ErrorReflectionDemo.idr
module ErrorReflectionDemo
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
data Col = BOOL | STRING | INT