einblicker

object Proof {
  type Not[A] = A => Nothing

  trait All[P[_]] {
    def apply[A]: P[A]
  }

  def DN[A](p: Not[Not[A]]): A =
    p(return (_: A))

einblicker

object Vec {
  object NotEq {
    class =!=[A, B]
    implicit def aNeqB[A, B] = new =!=[A, B]
    implicit def aNeqA1[A] = new =!=[A, A]
    implicit def aNeqA2[A] = new =!=[A, A]
  }
  
  object Nat {
    sealed trait Nat {

einblicker

data Seq a = Nil | Cons a (Seq (a,a))

-- 多相再帰の型推論は完全ではないので、
-- このように型アノテーションをコメントアウトすると
-- コンパイルできない
-- len :: Seq a -> Int
len Nil = 0
len (Cons x s) = 1 + 2 * (len s)

pair f (x,y) = (f x, f y)

einblicker

class Vec(list: List[Double]) {
  case class Value(list: List[Double])
  val value = Value(list)

  def sameLength(x: Vec#Value): Option[Value] = {
    if (x.list.length == list.length) Some(Value(x.list))
    else None
  }

  def innerProd(x: Value): Double = {

einblicker

package logic

object PropAst {
  type Id = String
  sealed abstract class Term
  case class Const(name: Id) extends Term {
    override def toString = name
  }
  case class Var(name: Id) extends Term {
    override def toString = name

einblicker

import scalaz._
import Scalaz._

object FreeMonad extends App {
  class FreeMonad[F[_]: Monad] {
    sealed abstract class Free[A]
    case class Val[A](value: A) extends Free[A]
    case class Wrap[A](value: F[Free[A]]) extends Free[A]
    implicit val freeMonad = new Monad[Free] {
      def pure[A](x: => A) = Val(x)

einblicker

object OperationalMonad extends App {
  class Operational {
    type instr[A] <: { def run: A }
    sealed abstract class Program[A] {
      def map[B](k: A => B) = flatMap(k andThen Lift.apply)
      def flatMap[B](k: A => Program[B]): Program[B] = {
        Bind(this, k)
      }
      def run: A
    }

einblicker

object ResumptionMonad extends App {
  sealed abstract class Resumption[A] {
    def map[B](k: A => B) = flatMap(k andThen Val.apply)
    def flatMap[B](k: A => Resumption[B]): Resumption[B] = {
      def loop(x: Resumption[A]): Resumption[B] =
        x match {
          case Val(value) => k(value)
          case Wrap(value) => Wrap(loop(value))
        }
      loop(this)

einblicker

object Test extends App {
  object Vec {
    def fromList[A](l: List[A]): Vec[_, A] = Vec(l)
  }

  case class Vec[Tag1, A] private (private val l: List[A]) {
    def toList = l
    
    def zipWith[Tag2, B, C](v: Vec[Tag2, B])(f: (A, B) => C)(implicit ev: Tag1 =:= Tag2) =
      Vec[Tag1, C](l.zip(v.l).map{case (a, b) => f(a, b)})

einblicker

object Test extends App {
  sealed trait Nat
  case class Zero private (dummy: Zero) extends Nat
  case class Succ[T <: Nat] private (dummy: Succ[T]) extends Nat

  sealed abstract class Vec[L <: Nat, +T]
  case object VNil extends Vec[Zero, Nothing]
  case class VCons[L <: Nat, +T](head: T, tail: Vec[L, T]) extends Vec[Succ[L], T]
  
  def fromList[T, R](l: List[T])(k: (Vec[A, T] forSome {type A <: Nat}) => R): R = {