6
어떻게 어떤 종류의 가족 F 및 G에 대한 예를 들어, forall 제약을 작성하려면 어떻게해야합니까? 그렇다면 작은 예제가 제공 될 수 있습니까? 나는 Forall을 사용해야한다고 생각합니다.는
Q
는
A
답변
6
예, 이것은 constraints을 사용하여 가능합니다. 그러나주의하십시오! 타입 패밀리가 중요하지 않다면 여러분이 주장하는 평등은 constraints에 대한 충분한 일반성을 가지고는 유지 될 것 같지 않습니다. x 및 y가 붙어 형의 가족 또한
type family X where {}
type family Y where {}
때 유형의 가족이 성공적으로 내가 특정 원하는 제약 조건이 어떠한 자유 변수가없는 것을 볼 수 감소 여부, 특히 고려하십시오. 잘하면, 그것은 단지 예일뿐입니다. 이와 같은 실제 닫힌 제약은 유용하지 않을 것입니다.
는Data.Constraint.Forall의 기본적인 유형 제품군은 Forall입니다. 이 특정 예제는 ForallT을 사용하여 좀 더 편리하게 처리 할 수 있지만 Forall을 사용하는 방법을 이해하는 것이 가장 중요합니다.
일반적으로 Forall p은 forall x . p x을 의미합니다. 매우 일반적으로 들리는 것은 아니지만 실제로는 p을 단계별로 작성하면됩니다. 당신은 찾는다
forall x y. G (F x y) ~ (x, y)
당신이 추구하는 관계를 표현하는 클래스를 정의함으로써 시작하십시오.
class G (F x y) ~ (x, y) => C x y
instance G (F x y) ~ (x, y) => C x y
이제
class Forall (C x) => D x
instance Forall (C x) => D x
이 Forall D를 사용하여 다음
과 (D x = forall y . C x y 당신이 읽을 수있는) (즉, forall x . D x가) 당신의 제약 조건을 표현하는 정의, 단계별로 갈 수 있습니다. Dict (D x)을 얻고 다시 Dict (C x y)을 얻으려면 inst을 사용해야합니다.
더 큰 유형의 제약 조건을 찾고 계십니까? 아니면 실제로 그 값이 같은지 확인 하시겠습니까? 자신이하려는 일에 대해 더 많은 정보를 제공하는 것이 도움이 될 수 있습니다. –
평등 자체를 나타내는 값을 찾고 있다면 equalityVal :: G (F x y) : ~ :(x, y); equalityVal = ... Refl ...''~ ~ :'with'Data.Type.Equality'가 작동합니까? 반면에 더 큰 타입에 대한 제약이 있다면'G (F x y) ~ (x, y) => ...'를 가질 수 없습니까? 나는 제약 패키지에서'Forall'은 보편적으로 구속 조건 ('(Forall p, pa) => a'와 같이)에 대해 양적으로 계량화 한 것입니다.'p'는'Num'와 같은 제약 조건 일 수 있습니다. 너가 찾고있는 것이면 (나는 정확하게 이해하고있다). –