Skip to content

Instantly share code, notes, and snippets.

Avatar

Gergő Érdi gergoerdi

View GitHub Profile
View monitor.rs
#![feature(lang_items)]
#![feature(fundamental)]
#![feature(intrinsics)]
#![feature(on_unimplemented)]
#![feature(optin_builtin_traits)]
#![feature(unboxed_closures)]
#![feature(associated_type_defaults)]
#![feature(asm)]
#![feature(abi_avr_interrupt)]
#![feature(unwind_attributes)]
View ScopeCheckingLC.agda
module _ where
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Nullary
open import Data.Empty
-- Untyped lambda calculus, with "weak" names
module _ where
View Printf.hs
{-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
import GHC.TypeLits
import GHC.Types
import Data.Singletons
import Data.Singletons.Prelude
data Format = Lit Symbol | Str | Shown Type
View Fib.hs
fib' :: (Integer, Integer) -> (Integer, Integer) -> Integer -> Integer
fib' (p, q) (x0, x1) n = go n (p, q) (x0, x1)
where
go 0 (p, q) (x0, x1) = x0
go n (p, q) (x0, x1) = if odd then go (n-1) (p, q) $! step (p, q) (x0, x1)
else go n' (p', q') (x0, x1)
where
(n', b) = n `divMod` 2
odd = not (b == 0)
View ParametrictyViaLFT.agda
-- https://stackoverflow.com/questions/34388484/parametricity-exploiting-proofs-in-agda
PolyFun : Set Set1
PolyFun A = {X : Set} A X A
open import Relation.Binary.PropositionalEquality
Parametricity : {A : Set} Set _
Parametricity {A} = {X Y} (f : PolyFun A) a x y f {X} a x ≡ f {Y} a y
@gergoerdi
gergoerdi / Shapeshifting.agda
Last active Dec 18, 2015
Canonical representation of polymorphic functions over containers (http://stackoverflow.com/a/34346484/477476)
View Shapeshifting.agda
open import Data.Product
open import Function using (_∘_; id)
data Cont : Set₁ where
_<|_ : (S : Set) (P : S Set) Cont
[_]C : Cont Set Set
[ S <| P ]C X = Σ[ s ∈ S ] (P s X)
View SystemF.agda
open import Data.List
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′) renaming (map to mapSum)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality
Con : Set Set
Con = List
data Var {A : Set} (t : A) : Con A Set where
here : : Con A} Var t (t ∷ Γ)
View PermutationFunsHigherKinded.idr
import Data.Vect
import Data.Fin
%default total
fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins
Permutation : Nat -> Type
View PermutationFuns.idr
import Data.Vect
import Data.Fin
%default total
fins : Vect n (Fin n)
fins {n = Z} = []
fins {n = S n} = FZ :: map FS fins
permutations : {n : Nat} -> Vect (fact n) (Vect n a -> Vect n a)
View Permutations.idr
import Data.Vect
%default total
permutations : Vect n a -> Vect (fact n) (Vect n a)
permutations [] = [[]]
permutations {n = S n} (x :: xs) = rewrite multCommutative (S n) (fact n) in
concat $ map (inserts x) (permutations xs)
where
inserts : a -> Vect k a -> Vect (S k) (Vect (S k) a)
You can’t perform that action at this time.