khibino

open import Agda.Builtin.Equality using (_≡_; refl)

data _×_  (A : Set) (B : Set) : Set where
  _,_ : A → B → A × B

infixr 6 _×_
infixr 6 _,_

data _⊎_ (A : Set) (B : Set) : Set where
  inl : A → A ⊎ B

khibino

--
-- Buggy a は、
--
--   「a を受け取った後の継続」
--
-- を与えると、最終的な Step を IO 内で返す計算である。
newtype Buggy a =
  Buggy
    { unBuggy :: (a -> IO Step) -> IO Step
    }

khibino

{-# LANGUAGE DeriveFunctor #-}
-- DSL1 via Free Monad

import Control.Monad.Trans.State

data Free f a
  = Pure a
  | Nest (f (Free f a))
  deriving Functor

khibino

import Control.Concurrent
import Control.Concurrent.Async
import Control.Concurrent.STM
import Control.Applicative
import Control.Monad

import Data.IORef

import Data.Set (Set)

khibino

{-
Modeled the following Haskell code in Agda
Confirmed that the Agda Termination Checker fails on it
https://github.com/khibino/dnsext/blob/95ae07de77174e8a6ea80f075412549222c9a900/dnsext-iterative/DNS/Iterative/Query/ResolveJust.hs#L550-L583
 -}

open import Agda.Builtin.Unit using (⊤; tt)
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.Char using (Char)
open import Agda.Builtin.List using (List; []; _∷_)

khibino

{-# LANGUAGE NumericUnderscores #-}

import Control.Concurrent
import Control.Concurrent.Async as Async
import Control.Exception

import DNS.Types

fromIOException :: String -> IOError -> DNSError
fromIOException tag ioe = NetworkFailure (SomeException ioe) tag

khibino

module Example where

data Nat where
  Zero :: Nat
  Succ :: Nat -> Nat

append :: [a] -> [a] -> [a]
append  []    ys = ys
append (x:xs) ys = x : (xs `append` ys)

khibino

---

有限体の性質

p を素数としたとき位数が pⁿ の有限体は同型を除いて一意. (Moore, E. H. (1896), "A doubly-infinite system of simple groups" section 3)

ここから位数が 2ⁿ の有限体 GF(2ⁿ) は一意.

khibino

open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)

record Monoid (m : Set) : Set where
  infixl 6 _⊕_
  field
    _⊕_ : m → m → m

    associativity : ∀{a b c} → ((a ⊕ b) ⊕ c) ≡ (a ⊕ (b ⊕ c))

khibino

module YonedaHO where

open import Agda.Primitive using (Level; lsuc; _⊔_)
open import Level using (lift)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; cong; cong-app)
open import Data.Product using (_×_; ∃; _,_; proj₂)

{- apply _≡_ for objects and morphisms for Locally Small Categories -}

{- morphism type definition -}