{{ message }}

Instantly share code, notes, and snippets.

Donnacha Oisín Kidney oisdk

Created May 17, 2021
View bft-hyperfunction-presentation.markdown

title: Hyperfunctions, Breadth-First Traversals, and Search author: Oisín Kidney patat: theme: codeBlock: [vividBlack] code: [vividBlack] incrementalLists: true eval: ruby:

Created Feb 20, 2021
View effects.hs
 {-# LANGUAGE GADTs, DataKinds, TypeOperators, FlexibleInstances, KindSignatures, RankNTypes, QuantifiedConstraints, FlexibleContexts #-} data Free (fs :: [(* -> *) -> * -> *]) (a :: *) where Pure :: a -> Free '[] a Effect :: f (Free fs) a -> Free (f ': fs) a instance Functor (Free '[]) where fmap f (Pure x) = Pure (f x) instance ((forall x. Functor x => Functor (f x))
Created Oct 15, 2020
View ReductionProblem.agda
 {-# OPTIONS --without-K #-} module ReductionProblem where open import Agda.Builtin.Nat using (Nat; suc; zero) open import Agda.Primitive using (_⊔_) open import Agda.Builtin.Equality using (_≡_; refl) -- The Acc type, defined as a record: record Acc {a r} {A : Set a} (R : A → A → Set r) (x : A) : Set (a ⊔ r) where
Created Sep 17, 2020
View container.hs
 {-# LANGUAGE UnicodeSyntax #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE UndecidableInstances #-} import Data.Kind import Data.Functor.Const
Created Apr 22, 2020
View selective-countable.hs
 -- Selective lets us do "monadic" binds where the domain is restricted -- to the countable types (which can be infinite). {-# LANGUAGE TypeOperators #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ViewPatterns #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} import GHC.Generics
Last active Feb 12, 2020
View taba.hs
 {-# LANGUAGE DataKinds, GADTs, KindSignatures, PolyKinds, RankNTypes, ScopedTypeVariables, TypeOperators #-} import Data.Kind import Data.Coerce data Nat = Z | S Nat data Vec (a :: Type) (n :: Nat) where Nil :: Vec a Z (:-) :: a -> Vec a n -> Vec a (S n)
Created Jan 28, 2020
View catalan.hs
 {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveFoldable, DeriveTraversable, DeriveFunctor #-} import Data.List (mapAccumL) data Stream a = a :< Stream a deriving (Functor, Foldable, Traversable) infixr 5 :< instance Show a => Show (Stream a) where showsPrec n = showsPrec n . foldr (:) []
Created Jan 26, 2020
View brauntolist.hs
 import Test.QuickCheck import Data.Tree.Binary.Preorder (Tree(..), drawTree) import Control.Arrow (first) import Data.List (unfoldr) fromList :: [a] -> Tree a fromList xs = head (l (foldr f b xs 1 2)) where b _ _ ys zs = (repeat Leaf, (repeat Leaf, ys))
Last active Dec 29, 2019
View ids.hs
 {-# LANGUAGE DeriveFunctor, LambdaCase, BlockArguments, BangPatterns, RankNTypes, GeneralisedNewtypeDeriving, OverloadedLists, TypeFamilies #-} {-# OPTIONS_GHC -Wall #-} import Control.Monad import Control.Applicative import Numeric.Natural import GHC.Exts import GHC.Base (build)
Created Dec 27, 2019
View matrix.hs
 {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, NoStarIsType #-} {-# OPTIONS_GHC -Wall -fno-warn-unticked-promoted-constructors #-} import Data.Monoid (Sum(..)) import Data.Kind (Type) data Nat = Z | S Nat data Fin (n :: Nat) where