Skip to content

Instantly share code, notes, and snippets.

Henri Tuhola cheery

Block or report user

Report or block cheery

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@cheery
cheery / FiniteSets.idr
Created Sep 14, 2019
Idris translation of "Dependently typed programming with finite sets"
View FiniteSets.idr
||| The Idris translation of Denis Firsov's paper
||| "Dependently Typed Programming with Finite Sets"
||| http://firsov.ee/finset/finset.pdf
module FiniteSets
import Data.Fin
%default total
%access public export
@cheery
cheery / TransitiveClosure.idr
Created Sep 11, 2019
The transitive closure puzzle
View TransitiveClosure.idr
module TransitiveClosure
data Index : (xs : List a) -> Type where
Z : Index (x :: xs)
S : Index xs -> Index (x :: xs)
Uninhabited (Index []) where
uninhabited (Z) impossible
uninhabited (S _) impossible
@cheery
cheery / DependentImages.idr
Created Sep 9, 2019
Do we need dependent types to go dependent?
View DependentImages.idr
module DependentImages
import Data.Vect
-- I've been happening to stumble upon one idea, and learned that I can represent it in Idris.
-- Due to cumulativity constraint, the values in types aren't quite the values types treat.
-- We can think of it as having images of types that we handle.
data NatImage : Nat -> Type where
NZ : NatImage Z
NS : NatImage x -> NatImage (S x)
@cheery
cheery / Transitivity.idr
Created Sep 9, 2019
Transitivity puzzle
View Transitivity.idr
data Trans : (a -> a -> Type) -> a -> a -> Type where
Tri : p a b -> Trans p a b
Trs : Trans p a b -> Trans p b c -> Trans p a c
succ_rel : Nat -> Nat -> Type
succ_rel k j = (S k = j)
succ_rel_theorem : Trans Transitivity.succ_rel a b -> LT a b
succ_rel_theorem (Tri Refl) = LTESucc lteRefl
succ_rel_theorem (Trs x y) = let
@cheery
cheery / Parsing.idr
Created Sep 5, 2019
In case things crash somehow during upgrade, I stashed the whole Earley parser here for now.
View Parsing.idr
module Parsing
import ParsingHelpers
--import Data.List.Quantifiers
data Transition : (a -> a -> Type) -> a -> a -> Type where
IdTrans : (f x y) -> Transition f x y
StepTrans : (f x y) -> Transition f y z -> Transition f x z
rhs_head_transitive_closure : DecEq s => Grammar s -> List s -> List (Rule s)
rhs_head_transitive_closure g vs =
@cheery
cheery / Sets.idr
Created Sep 3, 2019
Universe inconsistency issue
View Sets.idr
module Sets
data Index : (xs : List a) -> Type where
Z : Index (x :: xs)
S : Index xs -> Index (x :: xs)
Uninhabited (Index []) where
uninhabited (Z) impossible
uninhabited (S _) impossible
@cheery
cheery / ParsingChallenge.idr
Created Aug 31, 2019
The parsing challenge in Idris
View ParsingChallenge.idr
module ParsingChallenge
-- The objective is the 'recognize' -function, on earley parsing style.
--Grammar : Type -> Type
--Generates : Grammar s -> s -> List s -> Type
--recognize : (g:Grammar s) -> (i:s) -> (s:List s) -> Dec (Generates g i s)
infixl 10 ::=
data Rule : Type -> Type where
(::=) : s -> (xs:List s) -> {auto nonempty:NonEmpty xs} -> Rule s
@cheery
cheery / LinearAbstractMachine.idr
Last active Aug 30, 2019
Linear abstract machine, written in Idris
View LinearAbstractMachine.idr
module LinearAbstractMachine
mutual
data U : Type where
Zero : U
One : U
Tensor : U -> U -> U
Func : U -> U -> U
Either : U -> U -> U
Prod : U -> U -> U
@cheery
cheery / Graphs.idr
Created Aug 28, 2019
Non-total, non-checked implementation of transitive closure
View Graphs.idr
module Graphs
Graph : Type -> Type
Graph v = List (v, v)
edges : Eq v => Graph v -> v -> List v
edges [] y = []
edges ((a, b) :: xs) y with (a == y, b == y)
| (False, False) = edges xs y
| (False, True) = a :: edges xs y
@cheery
cheery / Chu.idr
Last active Aug 28, 2019
Chu construction, third attempt
View Chu.idr
module Chu
-- Examining Chu construction again, this time in Idris.
data Prop : Type where
Unit : Prop
Counit : Prop
AC : Prop -> Prop -> Prop
AD : Prop -> Prop -> Prop
MC : Prop -> Prop -> Prop
You can’t perform that action at this time.