자, 하나씩합시다.

가치

가치는 프로그램이 평가하고 저글링하는 구체적인 데이터입니다. 공상이 아님, 몇 가지 예는

• 1
• true
• "fizz buzz foo bar"

종류

유형에 대한 좋은 설명은 “값 분류기”입니다. 유형은 런타임에 해당 값이 무엇인지에 대한 약간의 정보이지만 컴파일 타임에 표시됩니다.

예를 들어, 당신은 나에게 그렇게 말한다면 e : bool컴파일시에, 나는 그 알 e중 하나입니다 true또는 false런타임시, 아무것도! 타입은 이런 식으로 값을 잘 분류하기 때문에이 정보를 사용하여 프로그램의 기본 속성을 결정할 수 있습니다.

예를 들어, 내가 지금까지 당신이 추가를 참조하는 경우 e와 e'때 e : int와 e' : String나는 뭔가 비트 꺼져 알고있다! 사실 나는 이것을 플래그 지정하고 컴파일 타임에 오류를 던질 수 있습니다. “이봐, 전혀 말이되지 않습니다!”.

더 강력한 유형 시스템은 더 흥미로운 값을 분류하는 더 흥미로운 유형을 허용합니다. 예를 들어, 어떤 기능을 고려해 봅시다

f = fun x -> x

꽤 분명 f : Something -> Something하지만 그게 뭐야 Something? 지루한 유형의 시스템에서와 같이 임의의 것을 지정해야합니다 Something = int. 보다 유연한 유형 시스템에서는 다음과 같이 말할 수 있습니다.

f : forall a. a -> a

즉 “어떤을 위해 말을하는 것입니다 a, f매핑 a에 a“. 이를 통해 f보다 일반적으로 사용 하고 더 흥미로운 프로그램을 작성해 보겠습니다 .

또한 컴파일러는 우리가 부여한 분류자를 실제로 만족하는지 검사 f = fun x -> true할 것입니다. 버그가 있으면 컴파일러가 그렇게 말할 것입니다!

tldr로; 형식은식이 런타임에있을 수있는 값에 대한 컴파일 시간 제약 조건입니다.

타입 생성자

일부 유형이 관련되어 있습니다. 예를 들어 정수 목록은 문자열 목록과 매우 유사합니다. 이것은 sort정수의 sort경우 문자열의 경우 와 거의 같습니다 . 우리는 차이점을 일반화하고 요구에 따라 구축함으로써 거의 동일한 유형을 구축하는 일종의 공장을 상상할 수 있습니다. 이것이 타입 생성자입니다. 유형에서 유형에 이르는 함수와 비슷하지만 조금 더 제한적입니다.

전형적인 예는 일반적인 목록입니다. 의 형식 생성자는 일반적인 정의 일뿐입니다.

 data List a = Cons a (List a) | Nil

이제 List유형 a을 해당 유형의 값 목록에 매핑하는 함수입니다 ! Java-land에서는 아마도 이것이 “일반 클래스”라고 생각합니다

유형 매개 변수

형식 매개 변수는 형식 생성자 (또는 함수)에 전달 된 형식입니다. 그냥 우리가 말하고 싶지만 값 레벨과 같은 foo(a)매개 변수가 a얼마나 같은 List a유형의 매개 변수가 있습니다을 a.

종류

종류는 조금 까다 롭습니다. 기본 개념은 특정 유형이 유사하다는 것입니다. 예를 들어, 우리는 모든 원시 타입 자바가 int, char, float…하는 모든 행동하라가 동일한 “유형”을 가지고있는 것처럼. 유형 자체에 대한 분류 자에 대해 말할 때를 제외하고는 분류자를 종류라고합니다. 그래서 int : Prim, String : Box, List : Boxed -> Boxed.

이 시스템은 유형이 값을 관리하는 방식과 같이 어디서 사용할 수있는 유형에 대한 구체적인 규칙을 제공합니다. 분명히 말이되지 않습니다

 List<List>

또는

 List<int>

Java에서는 List콘크리트 유형에 적용해야하므로 그렇게 사용할 수 있습니다! 우리가 그들의 종류를 보면 List : Boxed -> Boxed이후부터는 Boxed -> Boxed /= Boxed위의 오류입니다!

대부분의 경우 우리는 실제로 종류에 대해 생각하지 않고 “상식”으로 취급하지만 더 멋진 유형 시스템에서는 생각해야 할 중요한 것입니다.

내가 지금까지 말한 것에 대한 작은 그림

 value   : type : kind  : ...
 true    : bool : Prim  : ...
 new F() : Foo  : Boxed : ...

위키 백과보다 더 나은 독서

이런 종류의 것에 관심이 있다면 좋은 교과서를 투자하는 것이 좋습니다. 타입 이론과 PLT는 일반적으로 상당히 광범위하며 일관된 지식 기반이 없으면 몇 달 동안 아무데도 가지 않고 돌아 다닐 수 있습니다.

내가 가장 좋아하는 책 중 두 가지는

• 타입과 프로그래밍 언어-Ben Pierce
• 프로그래밍 언어의 실제 기초-Bob Harper

둘 다 제가 방금 이야기 한 내용을 아름답고 잘 설명 된 세부 사항으로 소개하는 훌륭한 책입니다.

---

답변