[functional-programming] 종속 입력이란 무엇입니까?

종속 유형을 사용 하면 컴파일 시간에 더 많은 논리 오류 를 제거 할 수 있습니다 . 이를 설명하기 위해 기능에 대한 다음 사양을 고려하십시오 .f

함수 f는 짝수 정수만 입력 해야합니다 .

종속 유형이 없으면 다음과 같이 할 수 있습니다.

def f(n: Integer) := {
  if  n mod 2 != 0 then
    throw RuntimeException
  else
    // do something with n
}

여기서 컴파일러 n는 실제로 짝수 인지 감지 할 수 없습니다 . 즉, 컴파일러의 관점에서 다음 표현식이 괜찮은지 감지 할 수 없습니다 .

f(1)    // compiles OK despite being a logic error!

이 프로그램은 실행되고 런타임에 예외를 발생시킵니다. 즉, 프로그램에 논리 오류가 있습니다.

이제 종속 유형을 사용하면 훨씬 더 많은 표현을 사용할 수 있으며 다음과 같이 작성할 수 있습니다.

def f(n: {n: Integer | n mod 2 == 0}) := {
  // do something with n
}

다음 n은 종속 유형 {n: Integer | n mod 2 == 0}입니다. 이것을 크게 읽는 것이 도움이 될 수 있습니다.

n 각 정수를 2로 나눌 수있는 정수 세트의 구성원입니다.

이 경우 컴파일러는 컴파일 타임에 홀수를 전달한 논리 오류를 감지 f하여 프로그램이 처음에 실행되지 않도록합니다.

f(1)    // compiler error

---

다음은 이러한 요구 사항을 충족 하는 함수를 구현하는 방법에 대한 Scala 경로 종속 유형 을 사용한 예시입니다 f.

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  {
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

핵심은 값 n이 다음과 같이 값 유형에 어떻게 나타나는지 확인 하는 proof것입니다 n.IsEven.type.

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

유형 n.IsEven.type 은 값 에 따라 다르 n므로 용어 종속 유형 이라고 말합니다 .