Last active
July 17, 2018 15:21
-
-
Save jto/05764f12efb6b0ac669aee0ab565b9ce to your computer and use it in GitHub Desktop.
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 modules { | |
// Modules examples taken from | |
// see https://www.cs.cmu.edu/~rwh/introsml/modules/sigstruct.htm | |
// structure IntLT = struct | |
// type t = int | |
// val lt = (op <) | |
// val eq = (op =) | |
// end | |
object IntLT { | |
type t = Int | |
def lt(n: Int, m: Int): Boolean = n < m | |
def eq_(n: Int, m: Int): Boolean = n == m | |
} | |
// structure IntDiv = struct | |
// type t = int | |
// fun lt (m, n) = (n mod m = 0) | |
// val eq = (op =) | |
// end | |
object IntDiv { | |
type t = Int | |
def lt(n: Int, m: Int): Boolean = (n % m) == 0 | |
def eq_(n: Int, m: Int): Boolean = n == m | |
} | |
object IntStructTests { | |
// The type of IntLT.lt is | |
// IntLT.t * IntLT.t -> bool, | |
val testLTltType: (IntLT.t, IntLT.t) => Boolean = IntLT.lt _ | |
val testLTDivType: (IntDiv.t, IntDiv.t) => Boolean = IntDiv.lt _ | |
// Since IntLT.t and IntDiv.lt are both bound to the type int, it is technically correct to consider IntLt.t to be of type | |
// IntDiv.t * IntDiv.t -> bool | |
val testLTltEquallity: (IntLT.t, IntLT.t) => Boolean = IntDiv.lt _ | |
// and also of type | |
// int * int -> bool. | |
val testLTIntEquallity: (Int, Int) => Boolean = IntDiv.lt _ | |
// This can be alleviated by opening the structure for use in a particular context | |
def ltAndEq(exp1: Int, exp2: Int, exp3: Int, exp4: Int): Boolean = { | |
import IntDiv._ | |
lt(exp1, exp2) && eq_(exp3, exp4) | |
} | |
// The typical compromise is to introduce a short (typically one letter) name for the structures in question to minimize the clutter of a long path. Thus we might write | |
def ltAndEqI(exp1: Int, exp2: Int, exp3: Int, exp4: Int): Boolean = { | |
import modules.{IntDiv => I} | |
I.lt(exp1, exp2) && I.eq_(exp3, exp4) | |
} | |
} | |
// structure PersQueue = struct | |
// type 'a queue = 'a list * 'a list | |
// val empty = (nil, nil) | |
// fun insert (x, (bs, fs)) = (x::bs, fs) | |
// exception Empty | |
// fun remove (nil, nil) = raise Empty | |
// | remove (bs, f::fs) = (f, (bs, fs)) | |
// | remove (bs, nil) = remove (nil, rev bs) | |
// end | |
object PersQueue { | |
type Queue[A] = (List[A], List[A]) | |
val empty = (Nil, Nil) | |
def insert[A](a: A, q: Queue[A]) = (a :: q._1, q._2) | |
object Empty extends Exception // ? | |
def remove[A](q: Queue[A]): (A, Queue[A]) = q match { | |
case (Nil, Nil) => throw Empty | |
case (bs, f :: fs) => (f, (bs, fs)) | |
case (bs, nil) => remove ((nil, bs.reverse)) | |
} | |
} | |
object PersQueueTests { | |
val q = PersQueue.empty | |
val q1 = PersQueue.insert(1, q) | |
val q2 = PersQueue.insert(2, q) | |
val (x2, _) = PersQueue.remove(q2) | |
val (x1, _) = PersQueue.remove(q1) | |
} | |
/** | |
* Signatures | |
*/ | |
// signature ORDERED = sig | |
// type t | |
// val lt : t * t -> bool | |
// val eq : t * t -> bool | |
// end | |
trait ORDERED { | |
type T | |
def lt(t0: T, t1: T): Boolean | |
def eq_(t0: T, t1: T): Boolean | |
} | |
// signature INT_ORDERED = sig | |
// type t = int | |
// val lt : t * t -> bool | |
// val eq : t * t -> bool | |
// end | |
trait INT_ORDERED { | |
type T = Int | |
def lt(t0: Int, t1: Int): Boolean | |
def eq_(t0: Int, t1: Int): Boolean | |
} | |
// signature QUEUE = sig | |
// type 'a queue | |
// val empty : 'a queue | |
// val insert : 'a * 'a queue -> 'a queue | |
// exception Empty | |
// val remove : 'a queue -> 'a * 'a queue | |
// end | |
trait QUEUE { | |
type Queue[_] | |
def empty[A]: Queue[A] | |
def insert[A](a: A, q: Queue[A]): Queue[A] | |
trait Empty extends Exception | |
def remove[A](q: Queue[A]): (A, Queue[A]) | |
} | |
/** | |
* Signature Ascription | |
*/ | |
object TransparentAscription { | |
// structure IntLT : ORDERED = struct | |
// type t = int | |
// val lt = (op <) | |
// val eq = (op =) | |
// end | |
val IntLt = | |
new ORDERED { | |
type T = Int | |
def lt(n: Int, m: Int): Boolean = n < m | |
def eq_(n: Int, m: Int): Boolean = n == m | |
} | |
// structure IntDiv : ORDERED = struct | |
// type t = int | |
// fun lt (m, n) = (n mod m = 0) | |
// val eq = (op =) | |
// end | |
val IntDiv = | |
new ORDERED { | |
type T = Int | |
def lt(n: Int, m: Int): Boolean = (n % m) == 0 | |
def eq_(n: Int, m: Int): Boolean = n == m | |
} | |
} | |
object OpaqueAscription { | |
// structure Queue :> QUEUE = struct | |
// type 'a queue = 'a list * 'a list | |
// val empty = (nil, nil) | |
// fun insert (x, (bs, fs)) = (x::bs, fs) | |
// exception Empty | |
// fun remove (nil, nil) = raise Empty | |
// | remove (bs, f::fs) = (f, (bs, fs)) | |
// | remove (bs, nil) = remove (nil, rev bs) | |
// end | |
val Queue: QUEUE = new QUEUE { | |
type Queue[A] = (List[A], List[A]) | |
def empty[A] = (Nil, Nil) | |
def insert[A](a: A, q: Queue[A]) = (a :: q._1, q._2) | |
object Empty extends Queue.Empty | |
def remove[A](q: Queue[A]): (A, Queue[A]) = q match { | |
case (Nil, Nil) => throw Empty | |
case (bs, f :: fs) => (f, (bs, fs)) | |
case (bs, nil) => remove ((nil, bs.reverse)) | |
} | |
} | |
import shapeless.test.illTyped | |
// Opaque ascription is so-called because the definition of 'a Queue.queue is hidden by the binding; | |
// the equivalence of the types 'a Queue.queue and 'a list * 'a list is not propagated into the scope of the binding | |
illTyped(""" | |
val x: Queue.Queue[Int] = (List[Int](1), List[Int](2)) | |
val y: (List[Int], List[Int]) = Queue.empty[Int] | |
""") | |
} | |
/** | |
* Functors | |
*/ | |
object Functors { | |
// http://www.cs.cmu.edu/~rwh/isml/book.pdf | |
// functor DictFun | |
// (structure K : ORDERED) :> | |
// DICT where type Key.t = K.t = | |
// struct | |
// structure Key : ORDERED = K | |
// datatype ’a dict = | |
// Empty | | |
// Node of ’a dict * Key.t * ’a * ’a dict | |
// val empty = Empty | |
// fun insert (None, k, v) = | |
// Node (Empty, k, v, Empty) | |
// fun lookup (Empty, ) = NONE | |
// | lookup (Node (dl, l, v, dr), k) = | |
// if Key.lt(k, l) then | |
// lookup (dl, k) | |
// else if Key.lt (l, k) then | |
// lookup (dr, k) | |
// else | |
// v | |
// end | |
trait DictFun { | |
type K | |
val Ordered: ORDERED { type T = K } | |
sealed trait Dict[A] | |
final class Empty[A] extends Dict[A] | |
final class Node[A](val key: K, val value: A, val n: Dict[A]) extends Dict[A] | |
def empty[A] = new Empty[A] | |
def insert[A](d: Dict[A], k: K, a: A) = ??? | |
def lookup[A](d: Dict[A], k: K) = ??? | |
} | |
object DictFun { | |
def apply[K0](o: ORDERED { type T = K0 }) = | |
new DictFun { | |
type K = K0 | |
val Ordered = o | |
} | |
} | |
val IntLtDict = DictFun[Int](TransparentAscription.IntLt) | |
val IntDivDict = DictFun[Int](TransparentAscription.IntDiv) | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment