This gist has been upgraded to a blog post here.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Reverse where | |
open import Data.List as List hiding (reverse) | |
open import Data.List.Properties | |
open import Relation.Binary.PropositionalEquality | |
record ReverseLike (reverse : ∀ {A : Set} → List A → List A) : Set₁ where | |
constructor rl | |
field | |
reverse0 : ∀ {A} → reverse {A} [] ≡ [] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
package Vect | |
import scala.language.higherKinds | |
sealed trait Nat | |
sealed trait Z extends Nat | |
sealed trait S[N <: Nat] extends Nat | |
trait Exists[A, +B[_ <: A]] { | |
type fst <: A |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import qualified Data.Searchable as S -- from infinite-search package | |
import Control.Applicative (liftA2) | |
import Data.Function (fix) | |
-- We will see that a function which takes codata as an argument is | |
-- not necessarily codata itself. Here we see an isomorphism between | |
-- total functions of type (Stream Bool -> a) and finite trees of the | |
-- shape (SBFunc a) (below), whenever a has decidable equality. | |
-- We will be using infinite lists as streams, pretending |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module hellofrege.JavaList where | |
data LinkedList a = native java.util.LinkedList where | |
native add :: Mutable s (LinkedList a) -> a -> ST s Bool | |
native get :: Mutable s (LinkedList a) -> Int -> ST s (Maybe a) | |
native new :: () -> STMutable s (LinkedList a) | |
fromFregeList :: [a] -> STMutable s (LinkedList a) | |
fromFregeList xs = LinkedList.new () >>= loop xs where | |
loop (x:xs) jlist = LinkedList.add jlist x >> loop xs jlist |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Simon Peyton-Jones | |
Phillip Wadler | |
Paul Chiusano | |
Tony Morris | |
Mark Hibberd | |
Edwin Brady | |
John Carmack | |
Conor McBride | |
Evan Czaplicki | |
Brian McKenna |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- http://benedictgaster.org/wp-content/uploads/2012/08/haskwork97.pdf | |
-- Polymorphic Extensible Records for Haskell (page 3) | |
type Monoid v r = Rec { plus :: v -> v -> v , id :: v | r } | |
type Group v r = Monoid v { inv :: v -> v | r } | |
type Ring v r = Group v { mult :: v -> v -> v , one :: v | r } | |
iMonoid :: Monoid Int {} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
object RefactorPuzzle { | |
case class IntRdr[+A](read: Int => A) { | |
def map[B](f: A => B): IntRdr[B] = | |
IntRdr(f compose read) | |
def flatMap[B](f: A => IntRdr[B]): IntRdr[B] = | |
IntRdr(n => f(read(n)).read(n)) | |
} | |
object IntRdr { |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;;; Clojure port of http://dysphoria.net/code/hindley-milner/HindleyMilner.scala | |
(ns hindley-milner | |
(:require [clojure.string :as str])) | |
(declare occurs-in? occurs-in-type?) | |
(defn map-state | |
"Evaluate a list of state monad values in sequence, producing | |
a list of the results of each evaluation." |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class Outer { | |
class Inner | |
type Type | |
} | |
trait Trait | |
object Object extends Outer { | |
val inner = new Inner | |
} | |
class OuterP[A] { | |
class InnerP[B] |