milessabin

object KindPoly {
  class Eq[A, B]
  
  object Eq {
    implicit def witness[A] = new Eq[A, A]
  }
  
  implicitly[Eq[{ type K = Int}, { type K = Int }]]
  implicitly[Eq[{ type K = Int}, { type K = String }]]               // Does not compile 

milessabin

object WitnessNatT {
  import shapeless._
  import TypeOperators._

  trait NatTRel[L1 <: HList, F[_], L2 <: HList, G[_]]

  object NatTRel {
    type ~??>[F[_], G[_]] = {
      type λ[L1 <: HList, L2 <: HList] = NatTRel[L1, F, L2, G]
    }

milessabin

scala> implicit val i = 23
i: Int = 23

scala> def foo[T](t : T)(implicit ev : T = "foo") = ev
foo: [T](t: T)(implicit ev: T)T

scala> foo(0)
res6: Int = 23

scala> foo("bar")

milessabin

/*
 * Copyright (c) 2012 Miles Sabin 
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software

milessabin

// Universal quantification is encoded in terms of quantifier-free
// assertions about an "abitrary" type (cp. "all swans are white" vs.
// "the arbitrary swan is white". Inspired by Kit Fine's 1985 "Reasoning
// with Arbitrary Objects", http://philosophy.fas.nyu.edu/object/kitfine.
// 
// Possibly also related to Oleg Kiselyov's "Interpreting types as
// abstract values", http://okmij.org/ftp/Computation/index.html#teval.

// What I wouldn't give for kind-polymorphism here ...
  

milessabin

// Internal function
def update[L1 <: HList, L2 <: HList](k: Key, fs: L1)(ts: L2 => L2)(implicit e: CoNatTRelAux[L1, Field, L2, Id])

// Function used by client                                                                                                       
def update[P1 <: Product, P2 <: Product, L1 <: HList, L2 <: HList, F](k: Key)(fs: P1)                                             
  (implicit
    h1: HListerAux[P1, L1],
    e: CoNatTRelAux[L1, Field, L2, Id],
    h2: HListerAux[P2, L2],
    t: TuplerAux[L2, P2],

milessabin

scala> import shapeless._
import shapeless._

scala> import Tuples._
import Tuples._

scala> def fst[P <: Product, H, T <: HList](p : P)(implicit hl : HListerAux[P, H :: T]) = hl(p).head
fst: [P <: Product, H, T <: shapeless.HList](p: P)(implicit hl: shapeless.HListerAux[P,shapeless.::[H,T]])H

scala> val l = List(("foo", "bar"), ("baz", "wibble"))

milessabin

object grow extends Poly1 {
  implicit def casePuppy = at[Puppy](_.grow)
  implicit def caseKitten = at[Cat](_.grow)
}

val y = Puppy() :: Kitten() :: HNil
val a = y map grow

milessabin

scala> def foo[A, B, C](a: SNat[A], b: SNat[B], c: SNat[C])(implicit ssum: SSum[A, B, C]) = ssum
foo: [A, B, C](a: shapeless.SNat[A], b: shapeless.SNat[B], c: shapeless.SNat[C])(implicit ssum: shapeless.SSum[A,B,C])shapeless.SSum[A,B,C]

scala> foo(2, 3, 5)
res0: shapeless.SSum[Int(2),Int(3),Int(5)] = $anon$1@53d76e96

scala> foo(2, 3, 7)
<console>:15: error: could not find implicit value for parameter ssum: shapeless.SSum[Int(2),Int(3),Int(7)]
              foo(2, 3, 7)
                 ^

milessabin

Welcome to Scala version 2.10.0 (Java HotSpot(TM) 64-Bit Server VM, Java 1.7.0_05).
Type in expressions to have them evaluated.
Type :help for more information.

scala> def foo = { println("foo"); "foo" }
foo: String

scala> def bar = { println("bar"); "bar" }
bar: String