Type Constructor 매개 변수에 대한 인터페이스 제약 조건이있는 Idris 종속 레코드

Question

idris에서 종속 레코드의 형식 생성자에 대한 매개 변수에 대한 인터페이스 제약 조건을 사용할 수 있습니까? 인터페이스가 Show : Type -> Type입니다. 지금은 다음에 의존 기록에 제약을 줄 필요가 :

record Source s where 
    constructor MkSource 
    initial : s 

내가 항상 Show의 인스턴스를해야한다 있도록 매개 변수 s에 제약을 줄 필요가있다. 이것을 달성하는 방법?

Answer 1

이드리스 무거운 개발하지만 이드리스 그룹이 최근 이메일에 따라 레코드 구문은 현재의 인터페이스를 가지는 형태를 제약 지원하지 않습니다

https://groups.google.com/forum/#!topic/idris-lang/HMeTylslyFc

대신 데이터 형식 구문을 사용해야합니다 , 예.

module Main 

data Source: Type -> Type where 
    MkSource: Show s => s -> Source s 


x: Source Int 
x = MkSource 3 

showSource: Source s -> String 
showSource (MkSource x) = show $ x 

testMe: (showSource $ Main.x = "3") 
testMe = Refl