Skip to content

Instantly share code, notes, and snippets.

View donovancrichton's full-sized avatar

Donovan Crichton donovancrichton

23 followers · 27 following
View GitHub Profile
@donovancrichton
donovancrichton / sigma_break.idr
Created July 24, 2020 21:31
Matching on different types error
%default total
data MyList : Type -> Type where
Nil : {a : Type} -> MyList a
(::) : {a : Type} -> a -> MyList a -> MyList a
F : MyList a -> Maybe Type
F [] = Nothing
F ((::) {a} x xs) = Just a
G : MyList a -> Maybe Type
@donovancrichton
donovancrichton / implicit_break.idr
Created July 26, 2020 09:07
Introducing implicits on the LHS works when an infix operator is matched in prefix form but fails to parse when introduced on a match in infix form.
data MyList : Type -> Type where
Nil : {a : Type} -> MyList a
(::) : {a : Type} -> a -> MyList a -> MyList a
f : MyList b -> ()
f [] = ()
f ((::) {a} x xs) = ?normal
g : MyList b -> ()
g [] = ()
@donovancrichton
donovancrichton / hf_full.idr
Last active July 29, 2020 06:03
Full specification of HF ZIpper as given (doesn't actually work)
-- Example 3.8 from Hanmana and Fiore - page 63
-- (Foundations of GADTS and Inductive Families)
data Expr : Type -> Type where
Const : Int -> Expr Int
IsZero : Expr Int -> Expr Bool
If : Expr Bool -> Expr a -> Expr a -> Expr a
-- Page 66: Context specialised for the Expr type above
-- General form for non-root cases is:
@donovancrichton
donovancrichton / hf_zipper_nat.idr
Created August 3, 2020 13:15
Example of HF Zipper breaking on Nat
%default total
ℕ : Type
ℕ = Nat
data D : ℕ -> Type where
K0 : D Z
K1 : {k : ℕ} -> D k -> D (S k)
K2 : {k : ℕ} -> D k -> D Z
data Ctx : ℕ -> Type where
@donovancrichton
donovancrichton / let_parser_type_fail.idr
Created August 4, 2020 05:39
Error when parsing let expressions of equality types.
f : (n : Nat) -> n = n + 0
f 0 = Refl
f (S k) =
let ih : k = plus k 0
ih = f k
in rewrite sym ih in Refl
@donovancrichton
donovancrichton / well-scoped.idr
Created September 28, 2020 04:52
An idris implementation of well-scoped lambda terms a la Allais et al.
{-
data Λ : List Type -> Type where
Var : (xs : List Type) -> Λ xs
Lam : Λ (x :: xs) -> Λ xs
App : Λ xs -> Λ xs -> Λ xs
-}
Scoped : Type -> Type
Scoped i = i -> List i -> Type
@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)
@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 / 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 / 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)