[haskell] Levity 다형성이란?

Program / 글쓴이

질문의 제목에서 알 수 있듯이 Levity 다형성이 무엇이며 그 동기가 무엇인지 알고 싶습니다. 나도 이 페이지는 거기에 몇 가지 세부 사항을 가지고 있지만, 설명의 대부분은 내 머리의 맨 위에이 이동합니다. 🙂

이 페이지 는 좀 더 친근 하지만 여전히 그이면의 동기를 이해할 수 없습니다.

답변

참고 : 이 답변은 Levity 토론에 대한 최근 관찰을 기반으로합니다. Levity 다형성과 관련된 모든 것은 현재 GHC 8.0 릴리스 후보에서만 구현되며 변경 될 수 있습니다 ( 예 : # 11471 참조 ).

TL; DR : 일반 함수로는 불가능한 해제 형과 해제 형에 대해 함수를 다형성으로 만드는 방법입니다. 예를 들어 다음 코드는 Int#has kind 이므로 일반 다형성으로 유형 검사를하지 #않지만의 유형 변수 id에는 kind가 있습니다 *.

{-# LANGUAGE MagicHash #-}

import GHC.Prim

example :: Int# -> Int#
example = id            -- does not work, since id :: a -> a

Couldn't match kind ‘*’ with ‘#’
When matching types
  a0 :: *
  Int# :: #
Expected type: Int# -> Int#
  Actual type: a0 -> a0
In the expression: id

참고 (->)여전히 마법을 사용합니다.

이 질문에 답하기 전에 한 발 물러서서 가장 자주 사용되는 함수 중 하나 인 ($).

($)유형 은 무엇입니까 ? Hackage와 보고서에 따르면

($) :: (a -> b) -> a -> b

그러나 그것은 100 % 완전하지 않습니다. 편리한 작은 거짓말입니다. 문제는 다형성 유형 (예 : a및 b)이 종류가 있다는 것 *입니다. 그러나 (라이브러리) 개발자들이 사용하고 싶었 ($)종류와 유형뿐만 *아니라 종류의 사람들을 위해 #, 예를 들어,

unwrapInt :: Int -> Int#

Int종류가 있는 동안 *(하단이 될 수 있음) Int#종류가 #있습니다 (하단이 될 수 없음). 그래도 다음 코드는 유형을 확인합니다.

unwrapInt $ 42

작동하지 않습니다. 반환 유형을 기억 ($)하십니까? 그것은 다형성이었고 다형성 유형에는 종류 *가 있습니다 #! 그렇다면 왜 작동했을까요? 첫 번째 는 버그 였고 그 다음은 해킹 이었습니다 ( ghc-dev 메일 링리스트에있는 Ryan Scott의 메일 발췌 ) :

그렇다면 왜 이런 일이 발생합니까?

긴 대답은 GHC 8.0 이전의 type signature ($) :: (a -> b) -> a -> b에서 b실제로는 종류 *가 아니라 오히려 OpenKind.
OpenKind해제 된 *(종류 #) 유형 과 해제되지 않은 (종류 ) 유형 모두에 서식 하도록 허용하는 끔찍한 해킹이므로 (unwrapInt $ 42)
typechecks입니다.

그렇다면 ($)GHC 8.0의 새로운 유형은 무엇입니까? 이것의

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.

이를 이해하려면 다음을 살펴보아야합니다 Levity.

data Levity = Lifted | Unlifted

이제 ($)다음 유형 중 하나를 갖는 것으로 생각할 수 있습니다 w.

-- pseudo types
($) :: forall a (b :: TYPE   Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b

TYPE마법 상수이며 종류를 재정의 *하고 #로서

type * = TYPE Lifted
type # = TYPE Unlifted

종류에 대한 정량화 도 상당히 새롭고 Haskell의 종속 유형 통합의 일부입니다 .

Levity 다형성 이라는 이름 은 이제 해제 된 유형과 해제되지 않은 유형 모두에 대해 다형성 함수를 작성할 수 있다는 사실에서 비롯됩니다. 이전의 다형성 제한에서는 허용 / 가능하지 않았습니다. 또한 동시에 OpenKind해킹을 제거합니다 . 이 두 종류를 모두 처리하는 것은 정말 “단지”입니다.

그건 그렇고, 당신은 당신의 질문에 혼자가 아닙니다. Simon Peyton Jones 조차 Levity wiki 페이지가 필요하다고 말했고 Richard E. (현재 구현 자) 는 wiki 페이지 에 현재 프로세스에 대한 업데이트가 필요하다고 말했습니다 .

참고 문헌

답변