유형 시스템을 사용하여 정수를 피아노 숫자로 변환

이것은 후속 조치 a question I asked almost two years ago입니다. 나는 벡터/행렬/텐서의 차원이 (Peano numbering을 가진) 타입 시스템을 사용하여 인코딩되는 작은 선형 대수학 라이브러리를 작성하기 위해 타입 시스템을 실험하고있다. 이를 통해 컴파일러는 이진 연산을 해당 차원의 객체로 제한 할 수 있습니다.유형 시스템을 사용하여 정수를 피아노 숫자로 변환

잘 작동하지만 각 치수 유형을 수동으로 지정해야합니다. 예를 들어 (shapeless natural numbers 사용) :

type _1 = Succ[Nat._0] 
type _2 = Succ[_1] 
type _3 = Succ[_2]

그것은 작은 크기 괜찮습니다하지만 크기 _1024를 정의해야하는 경우가 지루 가져옵니다. 나는 (성공없이) 대응하는 Peano-number 타입으로 정수 리터럴을 (컴파일 타임에) 변환하는 방법을 찾으려고 노력 중이다.

Daniel Sobral answer 개의 댓글에서 스칼라가 종속 유형을 지원하지 않았기 때문에 이것이 가능하지 않다고 들었습니다. 이제 Scala 2.10에는 종속 유형과 매크로가 모두 있습니다. 달성 할 수있는 방법이 있습니까?

출처

2013-01-07 paradigmatic

2.10에서는 def 매크로 만 지원하므로 매크로 파라다이스에서 유형 매크로를 살펴보아야합니다. http :// /docs.scala-lang.org/overviews/macros/paradise.html –

스칼라 지원 의존 유형? 그 배경을 좀 배울 수 있을까요? – Bill

@Bill은 매크로 예제를 살펴 봅니다. 매크로 결과 유형은 종속 유형입니다. – paradigmatic

매크로가 2.10.0 인 경우 가능합니다 (구문은 Paradise에서 더 깨끗해집니다).

val holder = NatExample.toNat(13)

그리고 :

scala> implicitly[holder.N =:= shapeless.Nat._13] 
res0: =:=[holder.N,shapeless.Nat._13] = <function1>

을 내가 예를 here 작업이 완료 오프 - 더 - 커프를 게시 한 - 난 확실히 쉽게 훨씬 더 간결-하는이처럼 사용할 수 있습니다 만들 수있는

리터럴이 아닌 정수 등을 전달하면 합당한 컴파일 타임 오류가 발생합니다.

출처

2013-01-07 12:31:11

이 문맥에서 = : = 연산자는 무엇을 의미합니까? –

컴파일러가 두 유형이 동일하다는 것을 알 수있는 증거를 제공하는 [표준 라이브러리 유형 클래스] (http://www.scala-lang.org/api/current/index.html#scala.Predef$)입니다. 그것이 사용 된 방법에 대한 논의는 2.10 이전에있었습니다 (예 : [this answer] (http://stackoverflow.com/a/3427759/334519) 참조). –

유형 시스템을 사용하여 정수를 피아노 숫자로 변환

답변

관련 문제