programing

스칼라 유형 프로그래밍 리소스

nasanasas 2020. 8. 19. 08:17
반응형

스칼라 유형 프로그래밍 리소스

이 질문 에 따르면 Scala의 유형 시스템은 Turing complete 입니다. 초보자가 유형 수준 프로그래밍의 장점을 활용할 수 있도록 어떤 리소스를 사용할 수 있습니까?

지금까지 찾은 리소스는 다음과 같습니다.

이러한 리소스는 훌륭하지만 기본이 누락 된 것 같아서 구축 할 탄탄한 기반이 없습니다. 예를 들어, 유형 정의에 대한 소개는 어디에 있습니까? 유형에 대해 어떤 작업을 수행 할 수 있습니까?

좋은 입문 자료가 있습니까?

개요

유형 수준 프로그래밍은 기존의 가치 수준 프로그래밍과 많은 유사점이 있습니다. 그러나 런타임에 계산이 발생하는 값 수준 프로그래밍과 달리 유형 수준 프로그래밍에서는 컴파일 타임에 계산이 수행됩니다. 나는 가치 수준에서의 프로그래밍과 유형 수준에서의 프로그래밍 사이의 유사점을 그리려고 노력할 것이다.

패러다임

유형 수준 프로그래밍에는 "객체 지향"과 "기능적"의 두 가지 주요 패러다임이 있습니다. 여기에서 링크 된 대부분의 예제는 객체 지향 패러다임을 따릅니다.

객체 지향 패러다임에서 유형 수준 프로그래밍의 훌륭하고 매우 간단한 예는 여기에 복제 된 apocalisp의 lambda 미적분 구현 에서 찾을 수 있습니다 .

// Abstract trait
trait Lambda {
  type subst[U <: Lambda] <: Lambda
  type apply[U <: Lambda] <: Lambda
  type eval <: Lambda
}

// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
  type apply[U] = Nothing
  type eval = S#eval#apply[T]
}

trait Lam[T <: Lambda] extends Lambda {
  type subst[U <: Lambda] = Lam[T]
  type apply[U <: Lambda] = T#subst[U]#eval
  type eval = Lam[T]
}

trait X extends Lambda {
  type subst[U <: Lambda] = U
  type apply[U] = Lambda
  type eval = X
}

예제에서 볼 수 있듯이 유형 수준 프로그래밍을위한 객체 지향 패러다임은 다음과 같이 진행됩니다.

  • 첫째 : 다양한 추상 유형 필드를 사용하여 추상 특성을 정의합니다 (추상 필드가 무엇인지 아래 참조). 이는 구현을 강요하지 않고 모든 구현에 특정 유형 필드가 존재하도록 보장하기위한 템플릿입니다. 람다 계산법의 예에서,이 대응 trait Lambda하는 보증은 다음과 같은 유형의 존재 : subst, apply,와 eval.
  • 다음 : 추상 특성을 확장하고 다양한 추상 유형 필드를 구현하는 하위 특성 정의
    • 종종 이러한 하위 특성은 인수로 매개 변수화됩니다. 람다 미적분 예제에서 하위 유형은 trait App extends Lambda두 가지 유형 ( S및 T, 둘 다의 하위 유형이어야 함 Lambda), trait Lam extends Lambda하나의 유형 ( T) 및 trait X extends Lambda(매개 변수화되지 않음 )으로 매개 변수화 된 하위 유형입니다 .
    • 유형 필드는 종종 subtrait의 유형 매개 변수를 참조하고 해시 연산자를 통해 유형 필드를 참조하여 구현되는 경우가 많습니다 #(점 연산자와 매우 유사 : .값). App람다 미적분 예제의 특성 에서 유형 eval은 다음과 같이 구현됩니다 type eval = S#eval#apply[T].. 이것은 본질적으로 eval특성의 매개 변수 유형을 S호출 하고 결과에 apply매개 변수 T를 사용하여 호출 합니다. 참고, S이 보장되는 eval매개 변수의 하위로를 지정하기 때문에 유형을 Lambda. 마찬가지로, 결과 eval필수는 가지고 apply가의 하위 유형으로 지정되어 있기 때문에, 유형을 Lambda추상적 특성에 지정된대로 Lambda.

기능적 패러다임은 특성으로 함께 그룹화되지 않은 매개 변수화 된 유형 생성자를 정의하는 것으로 구성됩니다.

가치 수준 프로그래밍과 유형 수준 프로그래밍의 비교

  • 추상 클래스
    • 가치 수준 : abstract class C { val x }
    • 유형 수준 : trait C { type X }
  • 경로 종속 유형
    • C.x (객체 C의 필드 값 / 함수 x 참조)
    • C#x (특성 C에서 필드 유형 x 참조)
  • 함수 서명 (구현 없음)
    • 가치 수준 : def f(x:X) : Y
    • 유형 수준 : type f[x <: X] <: Y( "유형 생성자"라고하며 일반적으로 추상 특성에서 발생)
  • 기능 구현
    • 가치 수준 : def f(x:X) : Y = x
    • 유형 수준 : type f[x <: X] = x
  • 조건문
  • 평등 확인
    • 가치 수준 : a:A == b:B
    • 유형 수준 : implicitly[A =:= B]
    • 값 수준 : 런타임시 단위 테스트를 통해 JVM에서 발생합니다 (즉, 런타임 오류 없음).
      • 본질적으로 주장은 다음과 같습니다. assert(a == b)
    • 유형 수준 : 유형 검사를 통해 컴파일러에서 발생합니다 (즉, 컴파일러 오류 없음).
      • 본질적으로 유형 비교입니다. 예 : implicitly[A =:= B]
      • A <:< B, compiles only if A is a subtype of B
      • A =:= B, compiles only if A is a subtype of B and B is a subtype of A
      • A <%< B, ("viewable as") compiles only if A is viewable as B (i.e. there is an implicit conversion from A to a subtype of B)
      • an example
      • more comparison operators

Converting between types and values

  • In many of the examples, types defined via traits are often both abstract and sealed, and therefore can neither be instantiated directly nor via anonymous subclass. So it is common to use null as a placeholder value when doing a value-level computation using some type of interest:

    • e.g. val x:A = null, where A is the type you care about

  • Due to type-erasure, parameterized types all look the same. Furthermore, (as mentioned above) the values you're working with tend to all be null, and so conditioning on the object type (e.g. via a match statement) is ineffective.

The trick is to use implicit functions and values. The base case is usually an implicit value and the recursive case is usually an implicit function. Indeed, type-level programming makes heavy use of implicits.

Consider this example (taken from metascala and apocalisp):

sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat

Here you have a peano encoding of the natural numbers. That is, you have a type for each non-negative integer: a special type for 0, namely _0; and each integer greater than zero has a type of the form Succ[A], where A is the type representing a smaller integer. For instance, the type representing 2 would be: Succ[Succ[_0]] (successor applied twice to the type representing zero).

We can alias various natural numbers for more convenient reference. Example:

type _3 = Succ[Succ[Succ[_0]]]

(This is a lot like defining a val to be the result of a function.)

Now, suppose we want to define a value-level function def toInt[T <: Nat](v : T) which takes in an argument value, v, that conforms to Nat and returns an integer representing the natural number encoded in v's type. For example, if we have the value val x:_3 = null (null of type Succ[Succ[Succ[_0]]]), we would want toInt(x) to return 3.

To implement toInt, we're going to make use of the following class:

class TypeToValue[T, VT](value : VT) { def getValue() = value }

As we will see below, there will be an object constructed from class TypeToValue for each Nat from _0 up to (e.g.) _3, and each will store the value representation of the corresponding type (i.e. TypeToValue[_0, Int] will store the value 0, TypeToValue[Succ[_0], Int] will store the value 1, etc.). Note, TypeToValue is parameterized by two types: T and VT. T corresponds to the type we're trying to assign values to (in our example, Nat) and VT corresponds to the type of value we're assigning to it (in our example, Int).

Now we make the following two implicit definitions:

implicit val _0ToInt = new TypeToValue[_0, Int](0)
implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) = 
     new TypeToValue[Succ[P], Int](1 + v.getValue())

And we implement toInt as follows:

def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()

To understand how toInt works, let's consider what it does on a couple of inputs:

val z:_0 = null
val y:Succ[_0] = null

When we call toInt(z), the compiler looks for an implicit argument ttv of type TypeToValue[_0, Int] (since z is of type _0). It finds the object _0ToInt, it calls the getValue method of this object and gets back 0. The important point to note is that we did not specify to the program which object to use, the compiler found it implicitly.

Now let's consider toInt(y). This time, the compiler looks for an implicit argument ttv of type TypeToValue[Succ[_0], Int] (since y is of type Succ[_0]). It finds the function succToInt, which can return an object of the appropriate type (TypeToValue[Succ[_0], Int]) and evaluates it. This function itself takes an implicit argument (v) of type TypeToValue[_0, Int] (that is, a TypeToValue where the first type parameter is has one fewer Succ[_]). The compiler supplies _0ToInt (as was done in the evaluation of toInt(z) above), and succToInt constructs a new TypeToValue object with value 1. Again, it is important to note that the compiler is providing all of these values implicitly, since we do not have access to them explicitly.

Checking your work

There are several ways to verify that your type-level computations are doing what you expect. Here are a few approaches. Make two types A and B, that you want to verify are equal. Then check that the following compile:

Alternatively, you can convert the type to a value (as shown above) and do a runtime check of the values. E.g. assert(toInt(a) == toInt(b)), where a is of type A and b is of type B.

Additional Resources

The complete set of available constructs can be found in the types section of the scala reference manual (pdf).

Adriaan Moors has several academic papers about type constructors and related topics with examples from scala:

Apocalisp is a blog with many examples of type-level programming in scala.

ScalaZ is a very active project that is providing functionality that extends the Scala API using various type-level programming features. It is a very interesting project that has a big following.

MetaScala is a type-level library for Scala, including meta types for natural numbers, booleans, units, HList, etc. It is a project by Jesper Nordenberg (his blog).

The Michid (blog) has some awesome examples of type-level programming in Scala (from other answer):

Debasish Ghosh (blog) has some relevant posts as well:

(I've been doing some research on this subject and here's what I've learned. I'm still new to it, so please point out any inaccuracies in this answer.)

In addition to the other links here, there are also my blog posts on type level meta programming in Scala:

As suggested on Twitter: Shapeless: An exploration of generic/polytypic programming in Scala by Miles Sabin.

Scalaz has source code, a wiki and examples.

참고URL : https://stackoverflow.com/questions/4415511/scala-type-programming-resources

반응형

'programing' 카테고리의 다른 글

PHP $ array [] = $ value 또는 array_push ($ array, $ value)에서 사용하는 것이 더 낫습니까?  (0) 2020.08.20
복사와 복제의 차이점은 무엇입니까?  (0) 2020.08.19
html (+ css) : 줄 바꿈을위한 선호 위치 표시  (0) 2020.08.19
xlsm 또는 xlsb 형식은 언제 사용해야합니까?  (0) 2020.08.19
DateTime 객체 반올림  (0) 2020.08.19

'programing'의 다른글

  • 현재글스칼라 유형 프로그래밍 리소스

관련글

댓글

티스토리툴바