Idris2+WebGL, 파트 #1: 안녕하세요 삼각형, 첫 번째 생각

나는 Idris 2에서 유형이 안전한 WebGL 애플리케이션을 만들어 종속 유형의 실질적인 의미를 탐구하기로 결정했습니다.

노력은 다소 혼란 스럽습니다. WebGL은 Vulkan 만큼은 아니지만 여전히 금속에 가깝습니다. 반면 고급 유형 시스템은 대부분 인간의 추론에 묶여 있습니다. 따라서 나는 주로 기존 명령에 제한을 추가할 것입니다. 일반적으로 나는 컴파일러가 하드웨어를 제어하고 프로그래머가 비즈니스 로직을 표현하도록 해야 한다고 주장하면서 이 접근 방식에 반대하지만, 종속 타이핑의 힘과 실제 어려움을 테스트하기 위해 복잡한 사례가 많은 좋은 연습처럼 보입니다.

FFI 기본 사항

JavaScript로 컴파일하는 것은 매우 간단하고 잘 문서화되어 있습니다. export IDRIS2_CG=javascript를 설정하면 완료됩니다.

JS 코드를 호출하는 것도 충분히 간단합니다. JavaScript에서 람다 식을 정의하고 Idris에서 이름과 유형을 지정하기만 하면 됩니다.

%foreign "browser:lambda: (gl, r, g, b, a) => gl.clearColor(r,g,b,a)"
prim__glClearColor : AnyPtr -> Double -> Double -> Double -> Double -> PrimIO ()

물론 JavaScript에는 실제로 유형이 없기 때문에 유형 표기법은 "저만 믿으세요"의 문제입니다.

그런 다음 primIO를 통해 기본 기능을 사용할 수 있습니다.

export
clearColor : HasIO io => GLContext -> Double -> Double -> Double -> Double -> io ()
clearColor (GLContextWrapper gl) r g b a = primIO $ prim__glClearColor gl r g b a

Idris의 FFI는 내 취향에 비해 너무 제한적입니다. The list of supported types is very limited . 몇 가지 유형만 지원해야 할 때 새 백엔드를 만드는 것이 더 쉽기 때문에 이는 의도된 것입니다. 실제로 그것은 예를 들어 사용하기 위해 농구를 뛰어 넘어야 함을 의미합니다. 부울 및 유형이 지정된 배열로 인해 최종 애플리케이션이 다소 느릴 수 있습니다.

export
data BufferDataSource = BufferDataSourceWrapper AnyPtr

%foreign "browser:lambda: size => new Float32Array(Number(size))"
prim__new_Float32Array_size : Int -> PrimIO AnyPtr

%foreign "browser:lambda: (a, i, v) => a[Number(i)] = v"
prim__set_Float32Array_at : AnyPtr -> Int -> Double -> PrimIO ()

-- NOTE: this could probably have been more succinct with a forM_ or similar. Haven't dived too deeply in the Idris packages yet.
fill_Float32Array : HasIO io => AnyPtr -> Vect _ Double -> io ()
fill_Float32Array f32a = fill_Float32Array_recursive 0
  where
    fill_Float32Array_recursive : Int -> Vect _ Double -> io ()
    fill_Float32Array_recursive idx vect =
      case vect of
        Nil => pure ()
        (v :: vs) => do
          primIO $ prim__set_Float32Array_at f32a idx v
          fill_Float32Array_recursive (idx + 1) vs

export
float32Array : HasIO io => {size : _} -> Vect size Double -> io BufferDataSource
float32Array vs = do
  typedArrayAnyPtr <- primIO $ prim__new_Float32Array_size (cast size)
  fill_Float32Array typedArrayAnyPtr vs
  pure $ BufferDataSourceWrapper typedArrayAnyPtr

나는 개인적으로 결정에 동의하지 않습니다. 외부 기능을 사용할 때 우리는 이미 프로그램을 특정 백엔드에 바인딩하고 있으므로 어쨌든 사용하지 않는 백엔드를 지원하기 위해 광범위하게 지원되는 제한된 목록을 사용하는 것보다 해당 백엔드가 사용 가능한 유형을 지시하도록 하는 것이 더 합리적입니다.

열거형의 경우 Idris 합계 유형을 사용하고 이를 문자열로 변환하여 JS에 전달합니다.

public export
data GLBufferTarget
  = GL_ARRAY_BUFFER
  | GL_ELEMENT_ARRAY_BUFFER
  | GL_PIXEL_PACK_BUFFER
  | GL_PIXEL_UNPACK_BUFFER
  | GL_COPY_READ_BUFFER
  | GL_COPY_WRITE_BUFFER
  | GL_TRANSFORM_FEEDBACK_BUFFER
  | GL_UNIFORM_BUFFER

bufferTargetStr : GLBufferTarget -> String
bufferTargetStr target =
  case target of
    GL_ARRAY_BUFFER => "ARRAY_BUFFER"
    GL_ELEMENT_ARRAY_BUFFER => "ELEMENT_ARRAY_BUFFER"
    GL_PIXEL_PACK_BUFFER => "PIXEL_PACK_BUFFER"
    GL_PIXEL_UNPACK_BUFFER => "PIXEL_UNPACK_BUFFER"
    GL_COPY_READ_BUFFER => "COPY_READ_BUFFER"
    GL_COPY_WRITE_BUFFER => "COPY_WRITE_BUFFER"
    GL_TRANSFORM_FEEDBACK_BUFFER => "TRANSFORM_FEEDBACK_BUFFER"
    GL_UNIFORM_BUFFER => "UNIFORM_BUFFER"

%foreign "browser:lambda: (gl, targetName, buffer) => gl.bindBuffer(gl[targetName], buffer)"
prim__bindBuffer : AnyPtr -> String -> AnyPtr -> PrimIO ()

export
bindBuffer : HasIO io => GLContext -> GLBufferTarget -> WebGLBuffer -> io ()
bindBuffer (GLContextWrapper gl) target (WebGLBufferWrapper buffer) =
  primIO $ prim__bindBuffer gl (bufferTargetStr target) buffer

대부분의 함수의 경우 JS/WebGL에서 값을 AnyPtr로 가져오고 추상 데이터 유형으로 래핑하여 매우 기본적인 유형 안전성을 얻습니다.

예를 들어 (거의) 모든 JS 값에 대해이 작업을 수행하는 것을 고려하고 있습니다. Number 및 Bool이므로 추가 변환이 필요하지 않습니다. 예를 들어 다음을 사용합니다.

export
data JSNumber = JSNumberWrapper AnyPtr

산술 등을 위한 FFI 바인딩

궁극적으로 추가 외부 함수 호출이 전환에 절약된 시간보다 중요한지 확실하지 않기 때문에 성능 테스트가 필요할 것입니다.

안녕하세요 삼각형

위의 내용을 염두에 두고 몇 가지 기능에 대한 바인딩을 만들었습니다. 화면에 삼각형을 표시하기에 충분했습니다.

미래의 걱정

몇 가지 걱정거리가 떠오릅니다. 대부분 성능입니다.

현재 접근 방식으로 인한 성능 저하 확인

JSNumber 와 같은 JS 값에 대한 유형을 사용하고 향후 성능 비교를 위해 WebGL 바인딩만 변경하여 기본 Idris 값으로 대체 가능하도록 만듭니다.

gl 컨텍스트는 JS에서처럼 클로저 기록에 더 적합할 수 있습니다. 구문은 JS에 더 가깝고 enum에 기본 값을 사용할 수 있습니다. 이로 인해 성능이 다시 저하될 수 있음

일부 기본 JS 최적화 단계는 Idris에서 컴파일된 코드에도 작동할 수 있습니다. 인라인이 도움이 될 수 있습니다.

아직 해야 할 일이 많습니다. 조금 더 그림을 그리고 문서화되었지만 입력되지 않은 규칙을 구현하기 시작했습니다.