[scala] Shapeless에서 Nat 유형의 한계

Program / 글쓴이

형태가없는 경우 Nat 유형은 유형 수준에서 자연수를 인코딩하는 방법을 나타냅니다. 예를 들어 고정 크기 목록에 사용됩니다. 유형 레벨에서 계산을 수행 할 수도 있습니다. 예를 들어 N요소 목록에 요소 목록을 추가하고 K컴파일시 알려진 목록을 가져와 N+K요소 를 갖습니다 .

이 표현이 많은 수 (예 : 10000002 53)를 표현할 수 있습니까 , 아니면 Scala 컴파일러가 포기하게됩니까?

답변

나는 스스로 시도 할 것이다. Travis Brown 또는 Miles Sabin의 더 나은 답변을 기꺼이 받아들입니다.

Nat는 현재 많은 수를 나타내는 데 사용할 수 없습니다

Nat의 현재 구현에서 값은 중첩 된 shapeless.Succ [] 유형의 수에 해당합니다.

scala> Nat(3)
res10: shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]] = Succ()

따라서 숫자 1000000을 나타내려면 1000000 레벨 깊이로 중첩 된 유형이 있어야 스칼라 컴파일러가 확실히 폭발 할 것입니다. 현재 한계는 실험에서 약 400으로 보이지만 합리적인 컴파일 시간에는 50 미만으로 유지하는 것이 가장 좋습니다.

그러나 계산을 원하지 않는 경우 큰 정수 또는 다른 값을 유형 수준으로 인코딩하는 방법이 있습니다 . 내가 아는 한 당신이 할 수있는 유일한 것은 그들이 같은지 여부를 확인하는 것입니다. 아래를 참조하십시오.

scala> type OneMillion = Witness.`1000000`.T
defined type alias OneMillion

scala> type AlsoOneMillion = Witness.`1000000`.T
defined type alias AlsoOneMillion

scala> type OneMillionAndOne = Witness.`1000001`.T
defined type alias OneMillionAndOne

scala> implicitly[OneMillion =:= AlsoOneMillion]
res0: =:=[OneMillion,AlsoOneMillion] = <function1>

scala> implicitly[OneMillion =:= OneMillionAndOne]
<console>:16: error: Cannot prove that OneMillion =:= OneMillionAndOne.
       implicitly[OneMillion =:= OneMillionAndOne]
                 ^

예를 들어 Array [Byte]에서 비트 연산을 수행 할 때 동일한 배열 크기를 적용하는 데 사용할 수 있습니다.

답변

Shapeless Nat는 교회 인코딩을 사용하여 유형 수준에서 자연수를 인코딩합니다. 다른 방법은 비트의 타입 레벨 HList로 내츄럴을 표현하는 것입니다.

이 솔루션을 형태없는 스타일로 구현 하는 고밀도 를 확인하십시오 .

나는 한동안 그것을 연구하지 않았으며 Lazy스칼라가 포기할 때 여기 저기 형태 가 없어야하지만 개념은 확실합니다. 🙂

답변