I hereby claim:
- I am rntz on github.
- I am rntz (https://keybase.io/rntz) on keybase.
- I have a public key whose fingerprint is DDAE CA21 888B 4735 408D 7838 9B09 FC8A FD28 2394
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
{-# LANGUAGE TypeFamilies, UndecidableInstances #-} | |
module Unwrap where | |
import Control.Monad | |
import Control.Monad.Except | |
import Control.Monad.Reader | |
import Control.Monad.State | |
import Data.Functor.Identity | |
class Unwrap m where |
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} | |
module Regex where | |
-- Something is a regex if it supports these methods. Laws not included. | |
-- Explained with grep-style notation: | |
-- | |
-- alt [A,B,...] = A|B|... | |
-- cat [A,B,...] = AB... | |
-- star A = A* | |
-- dot = . |
-------------------------------------------------------------------------------- | |
---------------------------------- THE SETUP ----------------------------------- | |
-------------------------------------------------------------------------------- | |
-- I like Agda's instance arguments, but I have a problematic use-case; it seems | |
-- like they'd be good for it, but I get an unexpected ambiguity. | |
open import Level | |
open import Data.Product |
# 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)] |
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 |
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 |
-- 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 |
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 |
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) |