параметрический GADT от внешнего

Question

GADT позволяет некоторую форму динамической типизации:

type _ gadt = 
    | Int: int -> int gadt 
    | Float: float -> float gadt 

let f: type a. a gadt -> a = function 
    | Int x -> x + 1 
    | Float x -> x +. 1. 

Я хотел бы быть в состоянии сделать тот же самый вид отправки, но с параметризованным типа с параметром gadt доступный снаружи. Если параметр квантором всеобщности, или фиксировано, это легко:

type (_,_) container = 
    | List: 'a list -> ('a,'a list) container 

let f : type a b. (a,b) container -> b = fun (List l) -> l 
let g : type a b. a -> (a, b) container -> b = fun x (List l) -> x::l 
let h : type b. (int, b) container -> b = fun (List l) -> 1::l 

Однако, если есть другие формы ограничений на параметр это не работает:

class ['a] ko (x:'a) = object 
    method m : type b. ('a, b) container -> b = fun (List l) -> x::l 
end 

Я получаю ошибку: Конструктор типа a # 0 покидает область действия. Я предполагаю, что это связано с внешним ограничением, без полного понимания домена.

Единственное решение, которое я нашел в том, чтобы использовать более высокий модуль:

open Higher 
module Higher_List = Newtype1 (struct type 'a t = 'a list end) 
type ('a,_) container = List: 'a list -> ('a, Higher_List.t) container 

class ['a] c (x:'a) = object 
    method m : type b. b container -> ('a,b) app = fun (List l) -> Higher_List.inj(x::l) 
end 

Это решение далеко от совершенства, однако: сначала многословен, с инъекц и Prj везде, и что более важно, есть много ограничения: «параметр не может иметь ограничений и дисперсии ...

Кто-нибудь знает о лучшем решении?

Редактировать

После некоторого мышления, решение Друп работает, но оно должно быть принято с осторожностью! В моей полной проблеме (а не игрушечной программе в этом вопросе) мне нужно иметь доступ к себе в определении метода. Поэтому, возвращаясь к решению Drup, я должен передать себя промежуточной функции, и для этого я должен указать тип. Поэтому я должен сначала объявить тип класса ...

class type ['a] c_type = object 
    method m: ('a, 'b) container -> 'b 
end 

let cons : type a b. a c_type -> a -> (a,b) container -> b = 
    fun self x (List l) -> x::l 

class ['a] c (x:'a) = object(self: 'a #c_type) 
    method m = cons (self :> 'a c_type) x 
end 

Это не будет работать, однако, если класс c есть ограничение на 'a: тип cons не будет действовать, как и a должны быть повсеместно количественно, но имеют предел в a c_type. Решение состоит в том, чтобы написать c_type без ограничения на 'a. Обратите внимание, что это означает много переписывания. Во многих случаях, просто опуская ограничение не достаточно, чтобы заставить его исчезнуть: все его использование должно быть непринужденность ...

Так окончательное решение выглядит следующим образом:

type (_,_) container = 
    | List: 'a list -> ('a,'a list) container 

class type ['a] c_type = object 
    (* no constraint on 'a, and take care of its usage ! *) 
    method m: ('a, 'b) container -> 'b 
end 

let cons : type a b. a c_type -> a -> (a,b) container -> b = 
    fun self x (List l) -> x::l (* in real code, self is used... *) 

class ['a] c (x:'a) = object(self: 'a #c_type) 
    constraint 'a = <..> (* well just for the example *) 
    method m = cons (self :> 'a c_type) x 
end 

Answer 1

Зачем пытаться сложным, когда вы можете сделать просто? :)

type (_,_) container = 
    | List: 'a list -> ('a,'a list) container 

let cons : type a b. a -> (a, b) container -> b = fun x (List l) -> x::l 

class ['a] ko (x:'a) = object 
    method m : type b. ('a, b) container -> b = cons x 
end 

Такие конструкции сложны, так как важно размещение локально абстрактного типа. В вашем случае вам нужен локально абстрактный тип на внешнем слое класса (для типа a), что невозможно. Обычно помогает промежуточная, правильно абстрагированная функция.

Кроме того, не используйте higher. Это доказательство того, что вы можете кодировать HKT в модульной системе, а не поощрять ее на самом деле.