시스템 FAQ 입력

Sit down, we need to talk about types

이 문장의 영감은사람들은 유형에 대해 많은 오해를 가지고 잘못된 용어를 사용해 잘못된 결론을 얻었다.나는 정적 유형 시스템을 제창하지 않는다. 나의 유일한 관심사는 우리가 정확한 용어를 사용하도록 하는 것이다. 그러면 우리는 건설적인 토론을 할 수 있다.
나는 자발적으로 이 글을 썼다.나는 잘못이 없기를 바라지만, 만약 당신이 무엇을 발견하면 나에게 알려 주세요.언제든지 더 많은 문제를 제기해 주십시오.우리들은 일하면서 영원히 이 문제를 해결합시다.

동적 및 비유형

어떤 사람들은 동적 유형 시스템이 비유형 시스템과 같다고 생각한다.이것은 정확하지 않다.비유형 유형 시스템은 유형을 구분하는 데 의미가 없는 시스템을 가리킨다.만약 한 가지 유형만 있다면, 유형을 구분하는 의미는 없다.예:

어셈블리 언어: 유일한 유형은 비트 문자열

lambda연산: 유일한 유형은lambdas

너는 이것이 동태적이든 비유형적이든 대수롭지 않다고 말할 수 있다.실제로 이것은 큰 문제이다. 왜냐하면 동적과 비유형을 동일시할 때 동적과 정적 유형 시스템을 자동으로 대립시키기 때문에 사람들은 동적과 정적 유형을 두 진영으로 나누기 때문이다. (이것은 정확하지 않다. 동적과 정적 참조)

Languages that do not restrict the range of variables are called untyped languages: they do not have types or, equivalently, have a single universal type that contains all values.

-- Type Systems, Luca Cardelli

Untyped — programs simply execute flat out; there is no attempt to check “consistency of shapes”

Typed — some attempt is made, either at compile-time or at run-time, to check shape-consistency

-- Type Systems for Programming Languages, Benjamin C. Pierce

동적 및 정적

동적 유형 시스템은 동적 검사 유형(실행 중)의 시스템입니다.
정적 유형 시스템은 정적 검사 유형 (컴파일하거나 전송할 때) 의 시스템입니다.
그들은 대립합니까?아니오, 그들은 아니에요.그들은 모두 유형에 관한 것이다.실제로 대부분의 정적 유형 시스템은 동적 유형 검사를 가지고 있다.예를 들어, 입출력 확인을 수행할 수 있습니다.사용자로부터 입력을 읽으려면 숫자를 입력해야 합니다.실행할 때 문자열의 해석이 숫자를 제공하는지 확인합니다. (이상을 일으키거나 NaN으로 되돌아갈 수 있습니다.)주어진 입력이 숫자로 볼 수 있는지 확인하려면 동적 형식 검사를 해야 합니다.
그래서 아니, 정태와 동태 유형의 전쟁이 아니야.둘 다 사용할 수 있습니다.
더 중요한 것은 정적 형식 검사는 복잡한 과정으로 때때로 정적 검증 프로그램의 일부분을 검증하기 어렵기 때문에 정적 형식 검사가 아니라 동적 형식 검사로 돌아갈 수 있습니다.
정적 유형 시스템을 정적 검사의 유형으로 간주합니다.
동적 유형 시스템을 동적 검사의 유형으로 간주합니다.

정적 형식은 컴파일할 때 형식을 알지 않습니까?

아니요. JS를 포함한 모든 해석기의 원본 코드를 열면 해석기가 해석할 때 알 수 있는 값의 유형을 볼 수 있습니다 (이것은 컴파일 과정의 일부입니다).

let x = "test";

해상도는 "test" 문자열이라는 것을 안다.이것이 JS를 정적으로 유형화할 수 있습니까?아니오

점진적 시스템

점진적 형식 시스템은 정적 형식 시스템으로 프로그램 부분의 형식 검사를 건너뛸 수 있습니다. 예를 들어 typescript의 any 또는 @ts-ignore 입니다.
한편으로는 안전성을 떨어뜨릴 수 있다.다른 한편, 점진적인 유형 시스템은 동적 유형 언어에 유형을 점차적으로 추가할 수 있다.

사운드 및 비사운드 유형 시스템

사운드 유형 관리자는 유형 오류가 있는 프로그램을 승인하지 않는 검사기입니다.따라서 잘못된 유형 검사기를 사용하면 응용 프로그램에서 유형 오류가 발생할 수 있습니다😱. 당황하지 마.사실 그것은 너에게 영향을 주지 않을 것이다.안정성은 유형 검사 알고리즘의 수학적 속성입니다. 이를 증명해야 합니다.많은 컴파일러 (안의 유형 검사기) 가 건전하지 않다.
사운드 형식 시스템을 사용하고 싶다면 ML 시리즈를 보십시오. Hindley-Milner 형식 시스템을 사용합니다.
사운드 형식 시스템은 잘못된 프로그램 (오보) 을 전달하지 않지만, 유효한 프로그램 (오보) 을 거부할 수도 있다는 것을 알아야 합니다.
유효한 프로그램을 거부하지 않는 형식 시스템을complete라고 합니다.
목소리와 온전한 것을 동시에 달라고 해도 될까요?내가 아는 바에 의하면 그것들은 결코 존재하지 않는다.나는 확실하지 않지만, 고델의 불완전성 정리에 따르면, 이것은 근본적으로 불가능한 것 같다.

약하다

나는 이 용어가 유용하다고 생각하지 않는다. 왜냐하면 그것은 애매모호하기 때문에 명확함보다 더 큰 혼란을 초래할 수 있기 때문이다.

These languages can be euphemistically called weakly checked (or weakly typed, in the literature) meaning that some unsafe operations are detected statically and some are not detected. Languages in this class vary widely in the extent of their weakness.

-- Type Systems, Luca Cardelli

Probably the most common way type systems are classified is "strong" or "weak." This is unfortunate, since these words have nearly no meaning at all. It is, to a limited extent, possible to compare two languages with very similar type systems, and designate one as having the stronger of those two systems. Beyond that, the words mean nothing at all.

-- What To Know Before Debating Type Systems, Steve Klabnik

The terms "strong" and "weak" are extremely ambiguous. Here are some ways that the terms are used:

• Sometimes, "strong" means "static". That's easy enough, but it's better to say "static" instead because most of us agree on its definition.
• Sometimes, "strong" means "doesn't convert between data types implicitly". For example, JavaScript allows us to say "a" - 1, which we might call "weak typing". But almost all languages provide some level of implicit conversion, allowing automatic integer-to-float conversion like 1 - 1.1. In practice, most people using "strong" in this way have drawn a line between "acceptable" and "unacceptable" conversions. There is no generally accepted line; they're all arbitrary and specific to the person's opinions.
• Sometimes, "strong" means that there's no way to escape the language's type rules.
• Sometimes, "strong" means memory-safe. C is a notable example of a memory-unsafe language. If xs is an array of four numbers, C will happily allow code that does xs[5] or xs[1000], giving whatever value happens to be in the memory addresses after those used to store xs.

-- Types - Programmer's Compendium, Gary Bernhardt

정적 형식 언어는 형식 설명을 필요로 합니까?

자꾸 이러는 거 아니야.때때로 유형 시스템은 유형을 추정할 수 있다. (코드 구조에 따라 추측할 수 있다.)예를 들어,

const x = "test";

유형 시스템은 "test" 문자열이라는 것을 알고 있습니다. (해석 규칙 때문에)유형 시스템은 x이 상량이라는 것을 알고 있다. 예를 들어 값을 다시 부여할 수 없기 때문에 x는 문자열이라는 결론을 얻을 수 있다.
추가 예제 (프로세스):

const add = (x, y) => x / y
//                        ^ Cannot perform arithmetic operation because string [1] is not a number.
add(1, "2")

형식 검사자는 우리가 숫자와 문자열로 호출하는 것을 보았습니다 add. 이것은 정의로 거슬러 올라갈 수 있습니다.유형 검사자는 나눗셈 연산에 숫자를 입력으로 해야 한다는 것을 알고 있기 때문에 문자열을 입력 중 하나로 사용하는 것은 잘못된 것이라고 말한다.
형식 성명은 없지만 정적 형식 검사를 할 수 있습니다.현실 세계에서 조만간 유형을 써야 할 것이다. 왜냐하면 유형 시스템은 모든 것을 추측할 수 없기 때문이다.그러나 정적 형식 언어는 성명과 무관하며, 실행 시 이전의 형식 검사와 관련이 있습니다.

TypeScript가 JavaScript로 컴파일되어 안전하지 않습니까?

TypeScript는 신뢰할 수 없기 때문에 안전하지 않은 응용 프로그램을 만들 수 있지만 컴파일의 목적과는 무관합니다.
데스크톱 컴파일러에 사용되는 대부분의 컴파일러는 JS¯\_(ツ)_/¯보다 보안이 떨어지는 어셈블리 언어를 사용합니다.
질문할 수 있습니다. 그러나 컴파일된 코드가 브라우저에서 실행됩니다. JS는 안전하지 않습니다. 예를 들어 문자열이 필요할 때null 값을 제공할 수 있습니다.
좋은 질문.따라서 TS는 어플리케이션 내부의 보안을 보장합니다. TS가 외부 세계와 상호작용하는 곳에'방호 장치'를 설정해야 합니다. 예를 들어 사용자 입력, 서버 응답, 브라우저 저장소에서 읽기 등 IO(입력-출력)를 검증해야 합니다.
예를 들어, Elm에서는 이 점을 구현하기 위해 "ports" 을 사용합니다.TS에서는 io TS 또는 유사한 기능을 사용할 수 있습니다.
이런'보호'는 정적 유형 시스템과 동적 유형 시스템 사이에 다리를 세웠다.
단순화 예:

const makeSureIsNumber = (x: any) => {
  const result = parseFloat(x);
  if (isNaN(result)) {
    throw Error("Not a number");
  }
  return result;
}
const read = (input: any) => {
  try {
    const n = makeSureIsNumber(input);
    // in this branch of code, n is for sure number
    // otherwise, we would get into a different branch of code
    // makeSureIsNumber "proofs" that n is number
  } catch (e) { }
}

형식은 단지 컴파일러에 필요한 것입니까?

Types are just a hack to give hints to your compiler.

-- Wout Mertens

이것은 철학 문제다.유형은 사람이 필요로 하는 것이지 기계가 필요로 하는 것이 아니다.컴파일러는 인류가 작성한 프로그램이기 때문에 유형이 필요하다.
유형이 현상으로서의 존재는 사람이 관찰하지 않으면 유형이 없기 때문이다.인간의 사유는 서로 다른 것을 서로 다른 통(또는 유형)에 넣는다.관찰자가 없으면 그들은 의미가 없다.
이것은 너에게 주는 사유 실험이다.인생 게임을 생각해 보세요.너는 정사각형 세포로 구성된 2차원 격자를 가지고 있는데, 모든 세포는 두 가지 가능한 상태 중의 하나, 살아 있거나 죽은 것이다.모든 세포는 8개의 인접 세포와 상호작용하는데, 이 세포들은 수평, 수직 또는 대각과 인접한다.각 시간 단계에서 다음과 같은 변환이 발생합니다.

두 명의 살아있는 이웃보다 적은 살아있는 세포는 모두 죽는다. 마치 인구 부족 때문인 것 같다.

두 개 또는 세 개의 살아있는 이웃의 살아있는 세포는 다음 세대까지 살아남는다.

세 명 이상의 살아있는 이웃의 살아있는 세포는 모두 죽는다. 마치 인구 과잉 때문인 것 같다.

세 명의 살아있는 이웃만 있는 어떤 죽은 세포도 번식을 통해 살아있는 세포로 변한다.

이것은 깜박임 (열기 및 닫기) 의 네모난 블록입니다.그것을 놀아라online.
하지만 당신은 약간의 구조를 가지고 있습니다. 예를 들어 글라이더:

보이시나요?이것은 글라이더가 스크린에서 움직이는 것 맞습니까?지금 멈춰.그것은 정말 존재합니까?그것은 단지 출현과 사라진 네모난 덩어리를 분리할 뿐이다.그러나 우리의 뇌는 하나의 실체로서의 구조를 관찰할 수 있다.
또는 우리는 그 존재가 정사각형이 독립적이지 않기 때문이라고 말할 수 있다. 글라이더 자체가 존재하지 않더라도 플라톤 사상의 글라이더로서의 개념은 존재한다.
이제 유형화된 프로그래밍 언어의 어떤 프로그램도 생각해 보세요.우리는 유형을 볼 수 있지, 그렇지?그러나 그것은 컴파일된 어셈블리 코드다.어셈블리 코드와 프로그램은 같은 것, 같은 논리를 대표한다.컴퓨터의 측면에서 볼 때 유형은 없고 비트 문자열인 0과 1(사세포와 활세포)의 집합만 있다.유형은 사람마다 존재한다.

덧붙이다

내가 이전에 쓴 유형의 시도:

https://github.com/stereobooster/pragmatic-types

그 글들은 업데이트와 수정이 필요합니다. 이 FAQ에 통합하고 싶습니다.

Cover image by reddit