[haskell] 의존적으로 타이핑하지 않는 이유는 무엇입니까?

의존적으로 입력 된 Haskell, 지금?

하스켈은 어느 정도 의존적으로 형식화 된 언어입니다. 타입 레벨 데이터에 대한 개념이 있는데, 이제 덕분에 더 잘 타이핑되었습니다 DataKinds. 그리고 GADTs타입 레벨 데이터에 런타임 표현을 제공하는 몇 가지 수단 ( )이 있습니다. 따라서 런타임 항목의 값이 types에 효과적으로 표시 되므로 언어를 종속적으로 입력해야합니다.

단순 데이터 유형은 종류 레벨 로 승격 되어 포함 된 값을 유형에 사용할 수 있습니다. 그러므로 전형적인 예

data Nat = Z | S Nat

data Vec :: Nat -> * -> * where
  VNil   :: Vec Z x
  VCons  :: x -> Vec n x -> Vec (S n) x

가능해지면서

vApply :: Vec n (s -> t) -> Vec n s -> Vec n t
vApply VNil         VNil         = VNil
vApply (VCons f fs) (VCons s ss) = VCons (f s) (vApply fs ss)

좋네요 길이 n는 해당 함수에서 정적으로 정적이므로 입력 및 출력 벡터의 길이는 동일하지만 실행 시간에는 아무런 영향을 미치지 않습니다
vApply. 반면에, 그것은 만드는 기능을 구현하는 (즉, 불가능) 훨씬 복잡합니다 n주어진의 사본 x(있을 것이다 pure에 vApply의 ‘를 <*>)

vReplicate :: x -> Vec n x

런타임에 사본 수를 아는 것이 중요하기 때문입니다. 싱글 톤을 입력하십시오.

data Natty :: Nat -> * where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

모든 승격 가능한 유형의 경우, 값의 런타임 복제본에 의해 승격 된 승격 된 유형에 대해 인덱스 된 싱글 톤 패밀리를 구축 할 수 있습니다. Natty ntype-level의 런타임 사본 유형 n
:: Nat입니다. 우리는 지금 쓸 수 있습니다

vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy     x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)

따라서 런타임 레벨로 요크되는 유형 레벨 값이 있습니다. 런타임 사본을 검사하면 유형 레벨 값에 대한 정적 지식이 세분화됩니다. 용어와 유형이 분리되어 있지만 단일 톤 구조를 에폭시 수지의 종류로 사용하여 상 사이에 결합을 만들어 의존적으로 유형을 지정할 수 있습니다. 형식에 임의의 런타임 식을 허용하는 데는 먼 길이지만 아무것도 아닙니다.

불쾌한 무엇입니까? 무엇이 빠졌습니까?

이 기술에 약간의 압력을 가하고 흔들기 시작하는 것을 봅시다. 싱글 톤을 좀 더 암시 적으로 관리 할 수 ​​있어야한다는 생각이들 수도 있습니다.

class Nattily (n :: Nat) where
  natty :: Natty n
instance Nattily Z where
  natty = Zy
instance Nattily n => Nattily (S n) where
  natty = Sy natty

우리가 글을 쓸 수 있도록

instance Nattily n => Applicative (Vec n) where
  pure = vReplicate natty
  (<*>) = vApply

그것은 효과가 있지만 이제는 우리의 원래 Nat유형이 종류, 싱글 톤 패밀리 및 싱글 톤 클래스의 세 사본을 생성 했음을 의미합니다 . 우리는 명백한 Natty n가치와 Nattily n사전 을 교환하기 위해 다소 성가신 과정을 가지고 있습니다 . 더구나, Natty아닙니다 Nat: 우리는 런타임 값에 어떤 종류의 의존성이 있지만 우리가 처음 생각했던 유형에는 없습니다. 완전 의존형 언어는 의존형을 복잡하게 만듭니다!

한편, Nat승진시킬 수는 있지만 할 수 Vec는 없습니다. 인덱싱 된 유형으로 인덱싱 할 수 없습니다. 의존적으로 유형이 지정된 언어로 가득 찬 그런 제한은 없으며, 내 경력에서 의존적으로 유형이 지정된 과시로, 나는 1 층 색인을 만든 사람들을 가르치기 위해 대화에 2 층 색인의 예를 포함시키는 법을 배웠습니다. 카드 집처럼 접을 것을 기대할 수는 없습니다. 뭐가 문제 야? 평등. GADT는 생성자에게 특정 반환 유형을 명시적인 방정식 요구로 제공 할 때 달성 한 제약 조건을 암시 적으로 변환하여 작동합니다. 이렇게

data Vec (n :: Nat) (x :: *)
  = n ~ Z => VNil
  | forall m. n ~ S m => VCons x (Vec m x)

두 방정식 각각에서 양변은 종류가 Nat있습니다.

이제 벡터를 통해 색인을 생성 한 것과 동일한 변환을 시도하십시오.

data InVec :: x -> Vec n x -> * where
  Here :: InVec z (VCons z zs)
  After :: InVec z ys -> InVec z (VCons y ys)

된다

data InVec (a :: x) (as :: Vec n x)
  = forall m z (zs :: Vec x m). (n ~ S m, as ~ VCons z zs) => Here
  | forall m y z (ys :: Vec x m). (n ~ S m, as ~ VCons y ys) => After (InVec z ys)

이제 우리는 양측이 구문 적으로 구별되는 (그러나 아마도 똑같은) 종류를 갖는 장소 사이 as :: Vec n x와
방정식의 제약 조건을 형성 VCons z zs :: Vec (S m) x합니다. GHC 코어는 현재 이러한 개념을 갖추고 있지 않습니다!

무엇이 더 빠졌습니까? 음, 하스켈의 대부분은 유형 수준에서 누락되었습니다. 승격 할 수있는 용어의 언어에는 실제로 변수와 비 GADT 생성자가 있습니다. 일단 당신이 그것들을 가지고 type family있다면 , 기계는 타입 레벨 프로그램을 작성할 수있게합니다 : 그것들 중 일부는 당신이 용어 레벨에서 쓰는 것을 고려하는 기능과 매우 유사 할 것입니다 (예를 들어, Nat추가를 장착 하여 추가하기에 좋은 타입을 줄 수 있습니다 Vec) 그러나 그것은 우연의 일치입니다!

실제로 누락 된 또 다른 것은 값으로 유형을 색인화하는 새로운 기능을 사용 하는 라이브러리 입니다. 이 용감한 새로운 세상에서 무엇을 Functor
하고 Monad있습니까? 나는 그것에 대해 생각하고 있지만 여전히 할 일이 많이 있습니다.

타입 레벨 프로그램 실행

Haskell은 가장 의존적으로 유형이 지정된 프로그래밍 언어와 같이 두 가지
작동 의미가 있습니다. 런타임 시스템이 프로그램을 실행하는 방법이 있습니다 (닫힌 표현식 만 유형 삭제 후 최적화 됨). 그러면 유형 검사기가 프로그램을 실행하는 방식이 있습니다 (유형 식, “유형 클래스 Prolog”, 개방 표현식). Haskell의 경우, 실행되는 프로그램이 다른 언어로되어 있기 때문에 일반적으로 두 가지를 섞지 않습니다. 의존적으로 유형이 지정된 언어는 동일한 언어의 프로그램에 대해 별도의 런타임 및 정적 실행 모델을 갖지만 걱정할 필요는 없지만 런타임 모델을 사용하면 유형 삭제 및 실제로 증거 삭제를 수행 할 수 있습니다. 이것이 바로 Coq의 추출입니다.메커니즘은 당신을 제공합니다; Edwin Brady의 컴파일러는 최소한 Edwin Brady가하는 일입니다 (Edwin은 불필요하게 중복 된 값과 유형 및 증명을 지우지 만). 위상 구분은
더 이상 구문 범주 의 구별이 아닐 수 있지만 살아 있고 좋습니다.

의존적으로 타이핑 된 언어는 전체적으로, 타입 체커가 오래 기다리는 것보다 더 나쁜 것에 대한 두려움으로부터 프로그램을 실행할 수있게한다. Haskell의 의존도가 높아짐에 따라 정적 실행 모델이 무엇인지에 대한 질문에 직면하게됩니까? 하나의 접근법은 정적 실행을 총 함수로 제한하여 동일한 자유를 실행할 수는 있지만 데이터와 코 데이터를 구별 할 수 있도록 (최소한 유형 레벨 코드의 경우) 강제 할 수 있습니다. 종료 또는 생산성을 강화합니다. 그러나 이것이 유일한 접근법은 아닙니다. 우리는 계산을 통해 더 적은 수의 방정식을 만들어내는 비용으로 프로그램을 실행하는 것을 꺼리는 훨씬 약한 실행 모델을 자유롭게 선택할 수 있습니다. 그리고 실제로, 그것은 GHC가 실제로하는 일입니다. GHC 코어의 타이핑 규칙은 달리기를 언급하지 않습니다.
프로그램, 그러나 방정식에 대한 증거를 확인합니다. 코어로 변환 할 때 GHC의 제한 솔버는 타입 레벨 프로그램을 실행하려고 시도하여 주어진 표현식이 정규 형식과 동일한 증거를 약간 은빛으로 만듭니다. 이 증거 생성 방법은 예측할 수없고 불가피하게 불완전합니다. 예를 들어, 무서운 것처럼 보이는 재귀에 맞서 싸울 수 있습니다. 아마 현명 할 것입니다. 우리가 걱정할 필요가없는 것은 타입 IO
체커에서 계산을 실행하는 것 입니다. 타입 체커는 launchMissiles런타임 시스템과 동일한 의미 를 부여 할 필요는 없습니다
.

힌들리-밀너 문화

Hindley-Milner 타입 시스템은 많은 사람들이 구별의 차이를 볼 수없고 우연의 일치가 불가피하다고 가정하는 불행한 문화적 부작용으로 네 가지 구별의 진정한 우연의 일치를 달성합니다! 내가 무슨 소리 야?

• 용어 대 유형
• 명시 적으로 작성된 것 vs 암시 적으로 작성된 것
• 런타임 전 존재 vs 런타임 전 삭제
• 비 의존적 추상화 대 의존적 정량화

우리는 용어를 쓰고 유형을 유추 한 다음 지워 버리는 데 익숙합니다. 우리는 해당 유형 추상화 및 응용 프로그램이 자동 및 정적으로 발생하는 유형 변수를 수량화하는 데 익숙합니다.

이러한 구별이 맞지 않기 전에 바닐라 힌들리-밀 너와 너무 멀리 떨어져있을 필요는 없으며, 이는 나쁘지 않습니다 . 처음에는 몇 군데에 기꺼이 글을 쓰려고하면 더 흥미로운 유형을 가질 수 있습니다. 한편, 오버로드 된 함수를 사용할 때 유형 클래스 사전을 작성할 필요는 없지만 런타임에 해당 사전이 존재하거나 인라인되어 있습니다. 의존적으로 유형이 지정된 언어에서는 런타임에 단순한 유형 이상의 것을 지울 것으로 예상되지만 유형 클래스와 같이 암시 적으로 유추 된 값은 지워지지 않습니다. 예를 들어 vReplicate의 숫자 인수는 종종 원하는 벡터의 유형에서 추론 할 수 있지만 여전히 런타임에 알아야합니다.

이러한 우연의 일치가 더 이상 없기 때문에 어떤 언어 디자인 선택을 검토해야합니까? 예를 들어, Haskell이 forall x. t정량 자를 명시 적으로 인스턴스화하는 방법을 제공하지 않는 것이 맞 습니까? x타입 체커가 unifiying하여 추측 할 수 없다면 t, 우리는 무엇이 x되어야 하는지 말할 다른 방법이 없다 .

더 광범위하게, 우리는 “유형 추론”을 우리가 가지고 있거나 전혀 가지고 있지 않은 모 놀리 식 개념으로 취급 할 수 없습니다. 시작하려면 “일반화”측면 (Milner의 “let”규칙)을 분리해야합니다.이 규칙은 어리석은 기계가 “전문화”측면 (Milner ‘ “var “rule) 제약 조건 솔버만큼 효과적입니다. 최상위 유형은 추론하기가 더 어려워 질 것으로 예상되지만 내부 유형 정보는 쉽게 전파 할 수 있습니다.

하스켈의 다음 단계

우리는 유형과 종류 수준이 매우 비슷해 짐을보고 있습니다 (그리고 이미 GHC에서 내부 표현을 공유하고 있습니다). 우리는 그것들을 합칠 수도 있습니다. * :: *우리가 할 수 있다면 재미있을 것입니다 . 오래 전에 논리적으로 소리를 잃었을
때, 바닥을 허용했지만 유형
소리는 일반적으로 약한 요구 사항입니다. 확인해야합니다. 고유 한 유형, 종류 등의 수준이 있어야하는 경우 최소한 유형 수준 이상의 모든 항목을 항상 홍보 할 수 있습니다. 종류 수준에서 다형성을 다시 발명하는 대신 유형에 이미 존재하는 다형성을 재사용하는 것이 좋습니다.

우리는 단순화시킴으로써 제약 현재 시스템을 일반화한다 이종 방정식 a ~ b의 종류 a및
b구문이 일치하지 않는 (하지만, 동일한 검증을 할 수있다). 그것은 의존성을 훨씬 쉽게 다루는 오래된 기술입니다 (지난 세기의 논문에서). GADT의 표현식에 대한 제약을 표현할 수 있으므로 승격 할 수있는 것에 대한 제한을 완화 할 수 있습니다.

종속 함수 유형을 도입하여 싱글 톤 구성의 필요성을 제거해야합니다 pi x :: s -> t. 이러한 유형의 함수 는 유형과 용어 언어 (따라서 변수, 생성자 등) 의 교차점 에있는 유형의 모든 표현식에 명시 적 으로 적용될 수 있습니다 . 해당 람다 및 응용 프로그램은 런타임에 지워지지 않으므로 작성할 수 있습니다.s

vReplicate :: pi n :: Nat -> x -> Vec n x
vReplicate Z     x = VNil
vReplicate (S n) x = VCons x (vReplicate n x)

바꾸지 않고 Nat의해 Natty. 의 도메인은 pi모든 승격 가능한 유형이 될 수 있으므로 GADT를 승격 할 수있는 경우 종속 수량화 시퀀스 (또는 Britejn이라고하는 “망원경”)를 작성할 수 있습니다.

pi n :: Nat -> pi xs :: Vec n x -> ...

원하는 길이로

이 단계의 핵심은 약한 도구와 복잡한 인코딩을 사용하는 대신보다 일반적인 도구로 직접 작업 하여 복잡성 을 제거 하는 것입니다. 현재 부분 바이 인은 Haskell의 일종의 종속 유형의 이점을 필요한 것보다 더 비싸게 만듭니다.

너무 열심히?

의존성 유형은 많은 사람들을 긴장하게 만듭니다. 그들은 나를 긴장하게 만들지 만, 나는 긴장하는 것을 좋아하거나 적어도 어쨌든 긴장하지 않는 것을 느낍니다. 그러나 주제에 대해 무지한 안개가 있다는 것을 돕는 것은 아닙니다. 그 중 일부는 우리 모두가 여전히 배울 점이 많기 때문입니다. 그러나 덜 급진적 인 접근을지지하는 사람들은 사실이 전적으로 그들과 함께 있는지 확인하지 않고 의존적 유형에 대한 두려움을 떨쳐내는 것으로 알려져 있습니다. 나는 이름을 짓지 않을 것이다. 이러한 “불확실한 유형 검사”, “불완전한 투어링”, “단계 구분 없음”, “타입 삭제 없음”, “모든 곳에서 증거 없음”등 신화는 비록 쓰레기 일지라도 지속됩니다.

의존적으로 유형이 지정된 프로그램이 항상 올바른 것으로 입증되어야하는 것은 아닙니다. 프로그램의 기본 위생을 향상시켜 전체 사양을 따르지 않고도 유형의 추가 불변성을 적용 할 수 있습니다. 이 방향으로의 작은 단계는 종종 추가 증거 의무가 거의 없거나 전혀없이 훨씬 더 강력한 보증을 제공합니다. 의존적으로 유형이 지정된 프로그램이 필연적 으로 증명으로 가득 하다는 것은 사실이 아닙니다 . 실제로 필자는 일반적으로 내 정의 에 의문 을 제기 하는 신호로 내 코드에 증명을 제공 합니다 .

왜냐하면, 조음 증의 증가와 마찬가지로, 우리는 새로운 것뿐만 아니라 공정한 파울을 자유롭게 말할 수 있습니다. 예를 들어, 이진 검색 트리를 정의하는 많은 어리석은 방법이 있지만 이것이 좋은 방법 이 아니라는 것을 의미하지는 않습니다 . 자존심이 그것을 인정하도록 허약하더라도 나쁜 경험이 더 나아질 수 없다고 가정하지 않는 것이 중요합니다. 의존적 정의의 디자인은 학습을 필요로하는 새로운 기술이며, Haskell 프로그래머가 자동으로 전문가가되지는 않습니다! 그리고 어떤 프로그램이 파울지라도 다른 사람들이 공정한 자유를 거부하는 이유는 무엇입니까?

왜 아직도 Haskell을 귀찮게합니까?

나는 의존적 인 유형을 정말로 좋아하지만 대부분의 해킹 프로젝트는 여전히 Haskell에 있습니다. 왜? 하스켈에는 타입 클래스가 있습니다. 하스켈에는 유용한 라이브러리가 있습니다. Haskell은 효과가있는 프로그래밍을 처리 할 수 ​​있습니다 (이상적이지는 않지만). Haskell에는 산업 강도 컴파일러가 있습니다. 의존적으로 유형이 지정된 언어는 커뮤니티 및 인프라의 성장에있어 훨씬 초기 단계에 있지만 메타 프로그래밍 및 데이터 유형 제네릭 등을 통해 가능한 세대를 실질적으로 변화시켜 나갈 것입니다. 그러나 Haskell이 종속 유형을 향한 발걸음의 결과로 사람들이 무엇을하고 있는지 살펴보면 현재 언어의 발전을 통해 많은 이점을 얻을 수 있습니다.

답변

data Some :: (k -> *) -> * where
  Like :: p x -> Some p

fromInt :: Int -> Some Natty
fromInt 0 = Like Zy
fromInt n = case fromInt (n - 1) of
  Like n -> Like (Sy n)

withZeroes :: (forall n. Vec n Int -> IO a) -> IO a
withZeroes k = do
  Like n <- fmap (fromInt . read) getLine
  k (vReplicate n 0)

*Main> withZeroes print
5
VCons 0 (VCons 0 (VCons 0 (VCons 0 (VCons 0 VNil))))