Skip to content

Instantly share code, notes, and snippets.

View donovancrichton's full-sized avatar

Donovan Crichton donovancrichton

View GitHub Profile
@donovancrichton
donovancrichton / Category.idr
Last active December 2, 2023 04:22
Formalising categories with setoids à la Hu & Carrette
module Category
%default total
public export
-- Heterogenous binary relations
REL : Type -> Type -> Type
REL a b = a -> b -> Type
-- Homogenous binary relations
public export
@donovancrichton
donovancrichton / Syntax.idr
Last active January 19, 2023 04:43
Typeclass implicit magic?
module Syntax
%default total
namespace SR
public export
interface Semiring a where
constructor MkSemiring
---------------------------- OPERATIONS ------------------------------------
-- A semiring (R) has two binary operations:
@donovancrichton
donovancrichton / PigeonHole.idr
Created October 25, 2022 01:23
Pigeonhole Principle in Idris
module PigeonHole
import Data.Nat
import Data.Vect
%default total
data Elem : a -> Vect k a -> Type where
Here : Elem x (x :: xs)
There : Elem x xs -> Elem x (y :: xs)
@donovancrichton
donovancrichton / HurkersParadoxLoop.idr
Created September 5, 2022 02:11
Hurken's Paradox in Idris
module HurkensParadoxLoop
%default total
-- Caued by Type : Type
-- Negation, (x : A) -> ⊥
¬ : Type -> Type
¬ x = x -> Void
@donovancrichton
donovancrichton / CantPatternMatchOnDPair.idr
Created September 2, 2022 03:24
Non-covering case when pattern matching on dependent pair.
module CantPatternMatchOnDPair
%default total
data Expr : Type -> Type where
Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)
-- this should be covering
f : (a : Type ** Expr a) -> (b : Type ** Expr b)
@donovancrichton
donovancrichton / CantMatchOnSigmaFunc.idr
Last active September 1, 2022 01:29
Minimal Example of odd not covering error from matching on Sigma types.
module CantMatchOnSigmaFunc
%default total
data Expr : Type -> Type where
Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)
{-
f : (a : Type ** Expr a) -> (b : Type ** Expr b)
f (ty ** focus) =
@donovancrichton
donovancrichton / CantGoLeft.idr
Created August 31, 2022 23:22
Weird totality errors with dependent pairs on proofs of functions?
module CantGoLeft
%default total
data Expr : Type -> Type where
Val : {a : Type} -> a -> Expr a
Add : {a : Type} -> Num a => Expr a -> Expr a -> Expr a
App : {a, b : Type} -> Expr (a -> b) -> Expr a -> Expr b
Lam : {a, b : Type} -> (a -> Expr b) -> Expr (a -> b)
@donovancrichton
donovancrichton / VerifiedApplciative.idr
Created August 29, 2022 04:31
Issues with interface reduction of types in a mutual definition (Verified Applicative)
------------------------------- Base Imports ---------------------------------
import Syntax.PreorderReasoning -- for long proofs
import Data.List -- for list lemmas
------------------------------ Custom Imports --------------------------------
import VerifiedFunctor
--------------------------------- Pragmas ------------------------------------
%default total
%hide Prelude.(<$>)
%hide Prelude.Interfaces.(<*>)
@donovancrichton
donovancrichton / Test.idr
Created February 24, 2022 09:35
Not strictly positivite when using an equality proof inside a data type that has a forward declaration
%default total
data Foo : Type
-- comment out the next line to have things type check.
data Bar : Foo -> Foo -> Type
data Foo : Type where
MkFoo : Foo
data Bar : Foo -> Foo -> Type where
@donovancrichton
donovancrichton / fix.idr
Created July 22, 2021 06:06
Programing being checked as %default total when it probably should not be total.
%default total
data Fix : (Type -> Type) -> Type where
MkFix : f (Fix f) -> Fix f
F : Type -> Type
F x = x -> x
fix : Fix F -> Fix F
fix (MkFix f) = f (MkFix f)