이드리스

Question

에 순위-N 정량을하는

난 단지 다소 서투른 방법으로 이드리스 0.9.12에서 순위-N 유형을 수행 할 수 있습니다 이드리스 구문 분석 발생하기 때문에

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

내가, 유형 응용 프로그램있을 때마다 밑줄이 필요

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

아마 더 큰 문제는 내가 모두에서 높은 순위 종류의 클래스 제약을 할 수 있다는 것입니다 : 오류가 나는 (중첩)하게 암시 인수를 입력하려고 할 때. 나는 이드리스에 다음 하스켈 기능을 변환 할 수 없습니다 :

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

이 또한 하스켈 Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t입니다 Lens, 같은 종류의 타입 동의어로 이드리스 기능을 사용하여에서 저를 방지 할 수 있습니다.

위의 문제를 해결하거나 피할 수있는 방법은 없나요?

Answer 1

난 그냥 마스터에서 구현, 임의의 범위에 implicits 허용, 그리고 다음 hackage 릴리스에있을거야. 그것은 아직 잘 테스트되지 않았습니다!

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() 

분에서 주요 제약 당신이 최고 수준에서 제외하고, 직접적으로 암시 적 인자에 대한 값을 제공 할 수 없다는 것입니다 : 나는 적어도 다음과 같은 간단한 예제 및 몇 가지 다른 시도했다. 나는 결국 그것에 대해 뭔가를 할 것입니다. ...