Instantly share code, notes, and snippets.

# Henri Tuholacheery

• Sort options
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
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
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)
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
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 =
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
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
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
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
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.