It's not surprising that type-class resolution is not triggering
automatically in your code, because the keyword [class] doesn't appear
anywhere in the program! That is, you are not declaring any particular
type class as existing, and the [testable] argument to
[testable_testList] won't be marked as generated automatically.
Here's the idiomatic way to do it:
(* --- *)
fun id [a] (x: a): a = x
type assertion = transaction xbody
datatype test = Test of assertion | TestList of list test
(* class *)
structure Testable : sig
class testable
val mkTestable : t ::: Type -> (t -> test) -> testable t
val testIt : t ::: Type -> testable t -> t -> test
end = struct
type testable t = t -> test
fun mkTestable [t] (f : t -> test) = f
fun testIt [t] (f : testable t) = f
end
open Testable
(* instances *)
val testable_test: testable test = mkTestable id
val testable_testList [t] (_: testable t): testable (list t) =
let
fun testIt' (t1: list t): test =
TestList (List.mp testIt t1)
in mkTestable testIt'
end
(* --- *)
On 01/19/2015 08:05 AM, Gabriel Riba wrote:
(* --- *)
fun id [a] (x: a): a = x
type assertion = transaction xbody
datatype test = Test of assertion | TestList of (list test)
(* class *)
con testable t = {TestIt: t -> test}
fun mkTestable [t] (f: t -> test): testable t = {TestIt = f}
val testIt [t] (r: testable t): (t -> test) = r.TestIt
(* instances *)
val testable_test: testable test = mkTestable id
val testable_testList [t] (_: testable t): testable (list t) =
let
fun testIt' (t1: list t): test =
TestList (List.mp testIt t1) (* line with error *)
in mkTestable testIt'
end
(* --- *)
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
