GADT 헤드의 유형 변수는 의미가 있습니까?

두 가지 GADT 선언간에 차이점이 있습니까?GADT 헤드의 유형 변수는 의미가 있습니까?

data A a b where 
    ... 

data A :: * -> * -> * where 
    ...

출처

2016-11-24 rightfold

우수 질문을. 이것은 내 애완 동물이다. 나는 이름이 다른 곳과는 관련이없는 것처럼 보이는 이유를 궁금해했다. 이것은 Agdes/Coq와 같은 종속 시스템에서 사용되는 유도 형의 지표와 지표와는 매우 다릅니다. – chi

반대로 타입 타입 패밀리에서는'A * * -> * -> *'와'a 형 -> * -> *'타입의 차이점이 있습니다. A Int Bool = Char와 같은 인스턴스; A int Char = Bool'인데, 후자는 그렇지 않습니다. 'A Int = Maybe'. (type family A :: * -> *')에서 – chi

...과 같은 형식을 사용하더라도'a'라는 이름은 여전히 부적합합니다. 반면에'type family B b :: *'는 당신을 사용하지 못하게합니다. 'MaybeTBa'는'B 형 * :: * * '형으로 가능합니다. 전자는 [부분 유형 동의어 응용 프로그램] (http://stackoverflow.com/a/4923883/745903)입니다. ('LiberalTypeSynonyms'는 때때로이 제한을 피할 수 있습니다.) – leftaroundabout

차이는 없습니다. 하나는 헤더의 형태 변수를 언급하지가 같이 생성자 서명에 그들을 위해 다른 이름을 사용하는 데 필요한 것이라고 생각 : the GHC Users Guide 말한대로 ..., 그러나

data A :: * -> * -> * where 
    AN :: Num x => x -> b -> A x b 
    AS :: IsString s => s -> b -> A s b

하스켈 -98 스타일 데이터 형식 선언과 달리 data Set a where 헤더의 형식 변수에는 범위가 없습니다.

... 그리고 그렇게 이것은 또한 작동합니다

data A a b where 
    AN :: Num x => x -> b -> A x b 
    AS :: IsString s => s -> b -> A s b

출처

2016-11-24 13:45:17 duplode

사실 처음에는 가장 좋아하지만 항상 짧아서 게으르다. 나는 그것들을 연상시키는 이름을 문서화하는데 유용 할 수있다. – chi

나는 친절한 서명을 쓰는 것을 좋아하지 않기 때문에 두 번째 스타일을 선호합니다. –

구문에서 형식 변수를 생략 할 수 있었을 것이라고 추측하지만 부분적인 종류의 서명을 원했을 것입니다. – dfeuer

GADT 헤드의 유형 변수는 의미가 있습니까?

답변

관련 문제