tpolecat

Hi, looking for scalac flags?

This gist has been upgraded to a blog post here.

copumpkin

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} [] ≡ []

raichoo

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

luqui

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

mmhelloworld

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

techtangents

Simon Peyton-Jones
Phillip Wadler
Paul Chiusano
Tony Morris
Mark Hibberd
Edwin Brady
John Carmack
Conor McBride
Evan Czaplicki
Brian McKenna

joseanpg

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

tonymorris

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 {

bodil

;;; 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."

etorreborre

class Outer {
  class Inner
  type Type
}
trait Trait
object Object extends Outer {
  val inner = new Inner
}
class OuterP[A] {
  class InnerP[B]