[Ur] Implicit problem in typeclass recursive instance [testable t] -> testable (list t)

[Adam Chlipala]

I believe you were just missing the [@@] prefix for identifiers, to 
disable implicit argument resolution in particular cases.

structure Foldable : sig
     class foldable :: (Type -> Type) -> Type
     val mkFoldable : t ::: (Type -> Type) -> (a ::: Type -> b ::: Type ->
                      ((a -> b -> b) -> b -> t a -> b)) -> foldable t
     val foldr : t ::: (Type -> Type) -> a ::: Type -> b ::: Type ->
                 foldable t -> (a -> b -> b) -> b -> t a -> b
end = struct
     type foldable t = a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> 
t a -> b
     fun mkFoldable [t](f: a ::: Type -> b ::: Type -> (a -> b -> b) -> 
b -> t a -> b) = @@f
     fun foldr [t][a][b] (f: foldable t): (a -> b -> b) -> b ->
                                              t a -> b = f
end

open Foldable

val foldable_list : foldable list = mkFoldable @@List.foldr

On 01/23/2015 03:19 AM, Gabriel Riba wrote:
> I have another question about free type variables of class methods. I can
> make them work by bringing them to class parameters.
>
> (* Foldable *)
>
> structure Foldable : sig
>      class foldable :: (Type -> Type) -> Type -> Type -> Type
>      val mkFoldable : t ::: (Type -> Type) -> a ::: Type -> b ::: Type ->
>                       ((a -> b -> b) -> b -> t a -> b) -> foldable t a b
>      val foldr : t ::: (Type -> Type) -> a ::: Type -> b ::: Type ->
>                  foldable t a b -> (a -> b -> b) -> b -> t a -> b
> end = struct
>      type foldable t = fn a b => (a -> b -> b) -> b -> t a -> b
>      fun mkFoldable [t][a][b](f: (a -> b -> b) -> b -> t a -> b) = f
>      val foldr [t][a][b] (f: foldable t a b): (a -> b -> b) -> b ->
>                                               t a -> b = f
> end
>
> open Foldable
>
> val foldable_list [a][b]: foldable list a b = mkFoldable List.foldr
>
> (* --- *)
>
> Is there a way to define the free type variables of methods existentially or
> should I stick to the previous design?
>
> (* --- *)
>
> type foldable t = a :::Type -> b:::Type -> (a -> b -> b) -> b -> t a -> b
>
> (* --- *)