Làm rank-n định lượng trong Idris

Question

tôi chỉ có thể làm các loại cấp bậc n trong Idris 0.9.12 theo một cách khá vụng về:

tupleId : ((a : Type) -> a -> a) -> (a, b) -> (a, b) 
tupleId f (a, b) = (f _ a, f _ b) 

tôi cần những dấu gạch dưới bất cứ nơi nào có một ứng dụng loại, vì Idris ném phân tích cú pháp lỗi khi tôi cố gắng thực hiện các đối số kiểu (lồng nhau) ẩn:

tupleId : ({a : Type} -> a -> a) -> (a, b) -> (a, b) -- doesn't compile 

Một vấn đề lớn hơn có thể là tôi không thể làm hạn chế lớp ở các loại hạng cao hơn. Tôi không thể dịch các chức năng sau đây để Haskell Idris:

appShow :: Show a => (forall a. Show a => a -> String) -> a -> String 
appShow show x = show x 

này cũng ngăn cản tôi từ việc sử dụng các chức năng Idris as type đồng nghĩa với nhiều loại như Lens, đó là Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t trong Haskell.

Bất kỳ cách nào để khắc phục hoặc phá vỡ các vấn đề trên?

Answer 1

Tôi vừa mới triển khai thực hiện điều này một cách chính xác, cho phép liên kết trong phạm vi tùy ý và nó sẽ nằm trong bản phát hành hack tiếp theo. Nó chưa được thử nghiệm tốt! Tôi ít nhất đã thử các ví dụ đơn giản sau đây và một vài ví dụ khác:

appShow : Show a => ({b : _} -> Show b => b -> String) -> a -> String 
appShow s x = s x 

AppendType : Type 
AppendType = {a, n, m : _} -> Vect n a -> Vect m a -> Vect (n + m) a 

append : AppendType 
append [] ys = ys 
append (x :: xs) ys = x :: append xs ys 

tupleId : ({a : _} -> a -> a) -> (a, b) -> (a, b) 
tupleId f (a, b) = (f a, f b) 

Proxy : Type -> Type -> Type -> Type -> (Type -> Type) -> Type -> Type 

Producer' : Type -> (Type -> Type) -> Type -> Type 
Producer' a m t = {x', x : _} -> Proxy x' x() a m t 

yield : Monad m => a -> Producer' a m() 

Hạn chế chính ở phút là bạn không thể đưa ra giá trị cho các đối số ngầm trực tiếp, ngoại trừ ở cấp cao nhất. Tôi sẽ làm điều gì đó về điều đó cuối cùng ...