raichoo

class MMethod[M, A1, A2, R](f: (A1, A2) => R) {                                                                      
  def apply(a1: A1, a2: A2): R = f(a1, a2)
}

class MultiMethod {
  def apply[A1, A2, R](a1: A1, a2: A2)
                      (implicit mm: MMethod[this.type, A1, A2, R]): R =
    mm(a1, a2)

  // use a singleton type to attach the resulting implicit to our multimethod

raichoo

package nlist                                                                   

sealed trait Nat 
sealed trait Z extends Nat 
sealed trait S[A <: Nat] extends Nat 

sealed trait NList[A <: Nat, +B] {
  type Length = A 

  def zap[C](l: NList[Length, B => C]): NList[Length, C]

raichoo

package nlist
           
sealed trait Even[A <: Nat]

object Even {
  implicit def isEven[A <: Nat](implicit e: A#IsEven =:= True): Even[A] =
    new Even[A]{}
}

sealed trait Bool {

raichoo

case object One 

trait Zero[A] {
  def zero: A
}

object Zero {
  implicit val oneZero: Zero[One.type] = new Zero[One.type] {
    def zero: One.type = One 
  }

raichoo

import Data.IORef
import Control.Applicative

data CounterRep = CounterRep { x :: IORef Int }

newCounterRep = CounterRep <$> newIORef 0 

data Counter = Counter { get :: IO Int,
                         set :: Int -> IO () }

raichoo

import Control.Applicative
import Control.Monad.Fix

data CounterRep = CounterRep { x :: Int }

data Counter = Counter { get :: Int,
                         set :: Int -> Counter,
                         inc :: Counter }

counterClass = \rep ->

raichoo

case class Config(host: String, port: Int) {
  def prettyPrint(prefix: String, msg: String): String =
    List(prefix, ": ", msg, " on ", host, ":", port.toString).mkString
}

/**
  * Passing a configuration with implicits is like
  * working in the state monad. You can "put" a
  * new configuration even though we don't want that
  * to happen in this particular example. We don't 

raichoo

mutual
  namespace Even
    data EvenList : Set where
      Nil  : EvenList
      (::) : Nat -> OddList -> EvenList

  namespace Odd 
    data OddList : Set where
      (::) : Nat -> EvenList -> OddList 

raichoo

import scala.language.higherKinds

/*
 * The usual peano numbers with addtion and multiplication  
 */
sealed trait Nat {
  type Plus[N <: Nat] <: Nat
  type Mult[N <: Nat] <: Nat
}

raichoo

module Main

data HTMLElement : Type where
  Elem : Ptr -> HTMLElement

data NodeList : Type where
  Nodes : Ptr -> NodeList

query : String -> IO NodeList
query q = do