ghc 7.4를 읽은 후. 출시 전 노트와 Giving Haskell a Promotion 논문을 읽으면서, 나는 당신이 실제로 승격 된 타입으로 무엇을하는지 아직도 혼란 스럽다. 예를 들어, GHC 설명서 승진 데이터 유형에 다음과 같은 예제를 제공합니다 : 종류로 이것들을 사용하는 어떤 종류의 의존적 인 사용자를위한 데이터 유형 승격
data Nat = Ze | Su Nat
data List a = Nil | Cons a (List a)
data Pair a b = Pair a b
data Sum a b = L a | R b
이 있습니까
? 예제 (코드) 예제를 줄 수 있습니까?Nat은 예를 들어. 같은 길이 인 경우에만 추가 할 수있는 숫자 벡터를 구성하는 데 사용되며 컴파일 시간은입니다.
종이 자체 적어도 두 가지 예제가 있습니다
"1. 소개"말한다 : "예를 들어, 우리가 주장 레드 - 블랙 트리가 정말 가지고 [컴파일시] 보장 할 수있을 것 빨강 - 검정색 속성. "
"2.1 데이터 유형 승격"에서는 길이가 인덱싱 된 벡터 (즉, 컴파일 시간이 "범위를 벗어난 인덱스"오류가있는 벡터)에 대해 설명합니다.
예를 들어이 방향으로 이전 작업을 살펴볼 수도 있습니다. 형식이 안전한 이기종 목록 및 확장 가능 컬렉션을위한 HList 라이브러리 Oleg Kiselyov에는 많은 관련 작품이 있습니다. 또한 종속 유형을 사용한 프로그래밍 작업을 읽을 수 있습니다. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf에는 Agda의 유형 수준 계산을위한 소개 예제가 있지만, 이것들은 하스켈에도 적용될 수 있습니다.
대략적으로 목록의 경우 head에 더 정확한 유형이 제공됩니다. 대신
head :: List a -> a
의 그것은
head :: NotEmptyList a -> a
후자의 헤드 기능은 fomer보다 더 많은 형태 보증이다 : 그것은 컴파일러 오류가 발생할 것이기 때문에 그것은 빈 목록에 적용되지 않을 수 있습니다.
NotEmptyList와 같은 유형을 표현하려면 유형 수준 계산이 필요합니다. 함수 적 종속성을 가진 타입 클래스, GAGT 및 (인덱스 된) 타입 패밀리는 이미 haskell에 대한 약한 형태의 유형 수준 계산을 제공합니다. 언급 한 작업은이 방향으로 더 자세히 설명합니다.
Haskell98 유형 클래스 만 사용하여 구현하려면 http://www.haskell.org/haskellwiki/Non-empty_list을 참조하십시오.
좋은 질문입니다. 좋은 대답을 구성하는 한 가지 방법은 "cabal install she"을 할 때 얻는 예제 파일을 번역하는 것입니다. 독자를위한 운동으로 SHE 코드를 게시 할 수 있습니다. 유용할까요? 지금 당장 7.4를 설치하려고하고 있지만 Leopard를 실행하고 있으며 나쁜 결과가 두렵습니다. – pigworker
@pigworker, 나는 SHE 예제를 살펴 보았고 일부 부분을 고수했다. 그러나 "거짓에 대한 주석"이있는 단순한 SHE 예제도 좋을 것이다. – aleator