View MinimalNBE.hs
-- A simply-typed lambda calculus, and a definition of normalisation by
-- evaluation for it.
--
-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
--
-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
-- consider open terms with the environments left implicit/untyped). This was a
-- pain in the ass to figure out.
View omega-category.agda
open import Level
-- "Wok" stands for "weak omega kategory".
mutual
record Wok {i} (Obj : Set i) : Set (suc i) where
coinductive
constructor Wok:
infix 1 Hom
infixr 9 compo
field Arr : (a b : Obj) -> Set i
field Hom : (a b : Obj) -> Wok (Arr a b)
View stuff.agda
open import Relation.Nullary
open import Data.Product
open import Function
module _ {i j} {A : Set i} {B : A -> Set j} where
-- ∀¬ and ¬∃ are interprovable constructively:
¬∃→∀¬ : ¬ (Σ A B) a -> ¬ B a; ¬∃→∀¬ = curry
¬→¬∃ : (∀ a -> ¬ B a) -> ¬ Σ A B; ¬→¬∃ = uncurry
-- So in particular, ¬∀¬ and ¬¬∃ are interprovable:
View jim-pivarski-examples.df
-- https://stackoverflow.com/questions/38831961/what-declarative-language-is-good-at-analysis-of-tree-like-data
-- This is my attempt to implement your examples in a suitably extended
-- hypothetical version of Datafun.
-- 1. Currently Datafun only has sets, while SQL has bags/multisets. Some of your
-- queries would be nicer if Datafun supported bags; for example, with bags we
-- can express a `mean` function's type as:
--
-- mean : Bag Float -> Float
View Cast.agda
module Cast where
open import Level
record Convert {i j} (A : Set i) (B : Set j) : Set (i ⊔ j) where
field convert : A -> B
open Convert public
open Convert {{...}} public using () renaming (convert to cast)
View inheritance.agda
record A : Set1 where field obj : Set
record B : Set1 where
field {{super}} : A
open A super public
open A public
open B public
foo : A -> Set
View instance-issue.agda
-- Using Agda 2.5.2.
open import Level
open import Data.Product
open import Data.Nat
-- uses instance resolution to solve something
auto : {i}{A : Set i}{{X : A}} -> A
auto {{X}} = X
-- I use postulates for brevity only; I could implement these, but the
View wut.hs
import Control.Monad
data Wut a = Wut
instance Functor Wut where fmap = liftM
instance Applicative Wut where pure = return; (<*>) = ap
instance Monad Wut where
return _ = Wut
Wut >>= f = Wut
View graph-connectedness.agda
open import Data.Product
open import Data.Unit
open import Level
record Graph i j : Set (suc (i ⊔ j)) where
field node : Set i
field edge : (a b : node) -> Set j
open Graph public
View cycle_permutation.py
# this is python3
import random
# generates a cyclic permutation of length `n`
def cycle_permutation(n):
shuffled = list(range(n))
random.shuffle(shuffled)
graph = {shuffled[i]: shuffled[(i+1)%n] for i in range(n)}
return [graph[i] for i in range(n)]