developer tip

Haskell Weird Kinds : Kind of (->)는 ??

copycodes 2020. 11. 18. 09:18
반응형

Haskell Weird Kinds : Kind of (->)는 ?? ->? -> *


Haskell 종류를 실험하고, 종류를 얻으려고 할 때 ->이것이 나타났습니다.

$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude> 

예상 대신 * -> * -> *. ???사물 은 무엇입니까 ? 구체적인 유형 또는 "종류 변수"를 의미합니까? 또는 다른 것?


이들은 Haskell 종류 시스템의 GHC 특정 확장입니다. Haskell 98 보고서 는 단순한 종류의 시스템 만 지정합니다 .

... 유형 표현식은 두 가지 가능한 형식 중 하나를 취하는 여러 종류로 분류됩니다.

* 기호는 모든 nullary 형식 생성자의 종류를 나타냅니다. k1과 k2가 종류 인 경우 k1-> k2는 종류 k1을 취하고 종류 k2를 반환하는 종류의 종류입니다.

GHC는 이 시스템 을 일종의 하위 유형 지정으로 확장 하여 unboxed 유형 을 허용하고 함수 생성자가 종류에 대해 다형성이되도록합니다. GHC가 지원하는 종류의 격자는 다음과 같습니다.

             ?
             /\
            /  \
          ??   (#)
          / \     
         *   #     

Where:       *   [LiftedTypeKind]   means boxed type
             #   [UnliftedTypeKind] means unboxed type
            (#)  [UbxTupleKind]     means unboxed tuple
            ??   [ArgTypeKind]      is the lub of {*, #}
            ?    [OpenTypeKind]     means any type at all

ghc / compiler / types / Type.lhs에 정의 됨

특히:

> error :: forall a:?. String -> a
> (->)  :: ?? -> ? -> *
> (\\(x::t) -> ...)

마지막 예제에서 t :: ??(즉, unboxed 튜플이 아닙니다). 따라서 GHC를 인용하면 "종류 수준에서 약간의 하위 유형이 있습니다".

관심있는 영혼을 위해 GHC는 GADT, 새로운 유형 및 유형 계열에서 사용되는 강제 유형 및 종류 ( "유형 동등성에 대한 증거로 작동하는 유형 수준 용어", System Fc에서 필요로 함 )도 지원합니다.

참고 URL : https://stackoverflow.com/questions/3034264/haskell-weird-kinds-kind-of-is

반응형