rntz

Keybase proof

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:

rntz

{-# 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

rntz

{-# 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 = .

rntz

--------------------------------------------------------------------------------
---------------------------------- 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

rntz

# 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)]

rntz

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

rntz

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

rntz

-- 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

rntz

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

rntz

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)