Skip to content

Instantly share code, notes, and snippets.

Avatar

Donnacha Oisín Kidney oisdk

View GitHub Profile
View container.hs
{-# LANGUAGE UnicodeSyntax #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Kind
import Data.Functor.Const
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
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)
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 (:) []
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))
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)
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
View curry.agda
{-# OPTIONS --cubical --safe #-}
module Curry where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Data.Nat
View infnat.agda
data ω : Type₀ where
zero : ω
suc : ω ω
inf : ω
suc-inf : suc inf ≡ inf
ω′ : Type₀
ω′ = Maybe ℕ
zero′ : ω′
View init.hs
init :: [a] -> [a]
init xs = foldr f b xs Nothing
where
b Nothing = error "init: empty list"
b _ = []
f x xs Nothing = xs (Just x)
f y xs (Just x) = x : xs (Just y)
You can’t perform that action at this time.