loại Hiện sinh trong chức năng bậc cao

Question

Tôi đã có một chức năng có nhiệm vụ tính toán một số giá trị tối ưu của loại a wrt một số chức năng giá trị của loại a -> v

type OptiF a v = (a -> v) -> a 

Sau đó, tôi có một container mà muốn để lưu trữ như vậy một chức năng cùng với chức năng khác trong đó sử dụng các giá trị giá trị:

data Container a = forall v. (Ord v) => Cons (OptiF a v) (a -> Int) 

ý tưởng là bất cứ ai thực hiện một chức năng của loại OptiF a v không nên bị làm phiền với các chi tiết của v ngoại trừ việc nó' s một ví dụ của Ord.

Vì vậy, tôi đã viết một hàm có hàm giá trị như vậy và vùng chứa. Sử dụng OptiF a v nó nên tính giá trị wrt tối ưu val và cắm nó vào result chức năng của container:

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int 
optimize val (Cons opti result) = result (opti val) 

Cho đến nay rất tốt, nhưng tôi không thể gọi optimize, vì

callOptimize :: Int 
callOptimize = optimize val cont 
    where val = (*3) 
     opti val' = if val' 1 > val' 0 then 100 else -100 
     cont = Cons opti (*2) 

không biên dịch:

Could not deduce (v ~ Int) 
from the context (Ord v) 
    bound by a type expected by the context: Ord v => Int -> v 
    at bla.hs:12:16-32 
    `v' is a rigid type variable bound by 
     a type expected by the context: Ord v => Int -> v at bla.hs:12:16 
Expected type: Int 
    Actual type: Int 
Expected type: Int -> v 
    Actual type: Int -> Int 
In the first argument of `optimize', namely `val' 
In the expression: optimize val cont 

nơi dòng 12: 16-32 là optimize val cont.

Tôi có hiểu nhầm các loại tồn tại trong trường hợp này không? Có phải forall v trong tuyên bố của optimize có nghĩa là optimize có thể mong đợi từ a -> v bất cứ điều gì v muốn? Hoặc có nghĩa là optimize có thể không mong đợi gì từ a -> v ngoại trừ Ord v?

Điều tôi muốn là OptiF a v không được sửa cho bất kỳ v nào, bởi vì tôi muốn cắm vào một số a -> v sau này. Ràng buộc duy nhất tôi muốn áp đặt là Ord v. Thậm chí có thể diễn tả một cái gì đó như thế bằng cách sử dụng các loại tồn tại (hay bất kỳ thứ gì)?

Tôi đã đạt được điều đó với một kiểu chữ bổ sung cung cấp hàm optimize có chữ ký tương tự với OptiF a v, nhưng trông có vẻ xấu hơn nhiều so với sử dụng hàm bậc cao hơn.

Answer 1

Đây là điều dễ hiểu.

Những gì bạn có trong chữ ký optimize là không phải là một hiện tượng, nhưng phổ quát.

... kể từ existentials có phần lỗi thời dù sao, chúng ta hãy viết lại dữ liệu của bạn để hình thành GADT, mà làm cho điểm rõ ràng hơn như cú pháp cơ bản cũng giống như cho các chức năng đa hình:

data Container a where 
    (:/->) :: Ord v =>      -- come on, you can't call this `Cons`! 
    OptiF a v -> (a->Int) -> Container a 

Quan sát rằng Ord ràng buộc (ngụ ý rằng đây là forall v...) đứng bên ngoài chữ ký hàm biến kiểu tham số, tức là v là một tham số chúng ta có thể ra lệnh từ bên ngoài khi chúng ta muốn tạo một giá trị Container.Nói cách khác,

Đối với tất cả v trong Ordcó tồn tại các nhà xây dựng (:/->) :: OptiF a v -> (a->Int) -> Container a

đó là những gì làm phát sinh cái tên "hiện sinh gõ". Một lần nữa, điều này là tương tự như một chức năng đa hình bình thường.

Mặt khác, trong chữ ký

optimize :: (forall v. (Ord v) => a -> v) -> Container a -> Int 

bạn có một forall bên trong hạn chữ ký riêng của mình, có nghĩa là những gì cụ thể loại v thể mất trên sẽ được quyết định bởi callee, optimize, trong nội bộ - tất cả những gì chúng tôi có quyền kiểm soát từ bên ngoài là nó nằm trong số Ord. Không có gì "hiện sinh" về điều đó, đó là lý do chữ ký này sẽ không thực sự biên dịch với XExistentialQuantification hoặc XGADTs một mình:

<interactive>:37:26: 
    Illegal symbol '.' in type 
    Perhaps you intended -XRankNTypes or similar flag 
    to enable explicit-forall syntax: forall <tvs>. <type> 

val = (*3) rõ ràng không đáp ứng (forall v. (Ord v) => a -> v), nó thực sự đòi hỏi một trường hợp Num mà không phải tất cả Ord s có . Thật vậy, optimize không cần loại rank2: nó sẽ hoạt động với bất kỳ Ord -type v người gọi nào có thể cung cấp cho nó.

optimize :: Ord v => (a -> v) -> Container a -> Int 

trong trường hợp thực hiện của bạn không hoạt động nữa, mặc dù: kể từ (:/->) thực sự là một nhà xây dựng hiện sinh, nó cần phải chứa chỉ bất kỳOptiF chức năng, cho một số loại chưa biết v1. Vì vậy, người gọi tối ưu hóa có quyền tự do lựa chọn chức năng opti cho bất kỳ loại cụ thể nào như vậy và chức năng được tối ưu hóa cho bất kỳ loại cố định nào khác - không thể hoạt động!

Giải pháp mà bạn muốn là: Container không nên tồn tại, hoặc là! Chức năng opti sẽ hoạt động đối với bất kỳ loại nào trong số Ord, không chỉ cho một loại cụ thể. Vâng, như một GADT này trông gần giống như chữ ký phổ-định lượng bạn ban đầu đã cho optimize:

data Container a where 
    (:/->) :: (forall v. Ord v => OptiF a v) -> (a->Int) -> Container a 

Với mà bây giờ, tối ưu hóa các công trình

optimize :: Ord v => (a -> v) -> Container a -> Int 
optimize val (opti :/-> result) = result (opti val) 

và có thể được sử dụng như bạn muốn

callOptimize :: Int 
callOptimize = optimize val cont 
    where val = (*3) 
     opti val' = if val' 1 > val' 0 then 100 else -100 
     cont = opti :/-> (*2)