Idris2+WebGL, 6부: 안녕 IO monad, 안녕 GL monad

이전 항목 로그 다음에, 모든 함수를 선형 형식으로 다시 쓰는 것이 내 임무입니다.이 과정은 흥미롭지 않지만 선형 유형 시스템을 만드는 도전에 대한 견해를 가지게 되었습니다. 이 로그의 끝에서 여러분과 공유하겠습니다.
재구성한 후에 나는 다음과 같은 형식의 많은 함수를 얻었다.

clearColor : GLContext -> Double -> Double -> Double -> Double -> IO ()

WebGL 컨텍스트가 상수가 아닐 수도 있지만 컨텍스트에 대한 참조는 기본적으로 상수이기 때문에 이 방법은 현재 여전히 유효합니다.불행하게도, 이것은 모든 함수를IO monad에 연결합니다. 왜냐하면 GL 함수 사이에 뚜렷한 순서를 만들어야 하기 때문입니다.만약 우리가 이렇게 하지 않는다면, Idris는 모든 함수를 순수함수로 정확하게 보고, 우리 프로그램을 파괴하는 방식으로 조작할 수 있을 것이다.
입출력 리스트와 선형 유형을 사용하는 것은 좀 얄밉다.우리,AFAIK,pure의 선형 변수가 없습니다.IO구조 함수가 내보내지지 않았기 때문에>>=우리는 어느 곳에서 자신을 다시 정의해야 합니다..기본적으로 그것은 비선형일 뿐이다.또한 IO는 하나의 유형으로서 너무 광범위하다고 생각합니다.
GLcontext를 선형화하여 IO를 제거할 수 있습니다.

clearColor : (1 _ : GLContext) -> Double -> Double -> Double -> Double -> GLContext

그러나 이는 각 WebGL 함수에 대해 다른 출력 값을 추가하고 현재 전달해야 하는 도면 코드GLContext에 대한 템플릿 파일을 추가합니다.

foo : (1 _ : GLContext) -> (1 _ : GLProgram) -> (GLProgram, GLContext)
foo gl program =
  let
    gl = clearColor gl 0 0 0 0
    gl = clear gl
    (program, gl) = useProgram gl program
    ...
  in
    (program, gl)

대신 HasIO 인터페이스를 구현하지 않고 다음과 같은 기능을 제공하는 GL monad를 사용하고 싶습니다.

clearColor : Double -> Double -> Double -> Double -> GL ()

다음 코드가 생성됩니다.

foo : (1 _ : GLProgram) -> GL GLProgram
foo program = do
  clearColor 0 0 0 0
  clear
  program <- useProgram program
  ...
  pure program

IO가 어떻게 Idris에서 이루어졌는지 ((paper 2.5절에서) 봤는데, 엔진 뚜껑 아래에서 선형 유형을 사용하는 것을 알고 있기 때문이다.

-- A primitive IO action takes a (linear) world state and produces an IO Response
PrimIO : Type  -> Type
PrimIO a = (1 w : %World) -> IORes a

-- an IO Response consists of a value and a new (linear) world state
data IORes : Type -> Type where
  MkIORes : (result : a) -> (1 w : %World) -> IORes a

-- IO is just a wrapper around PrimIO
data IO : Type  -> Type where
  MkIO : (1 fn : PrimIO a) -> IO a

그래서 본질적으로 유형IO a의 함수는 유형(1 _ : %World) -> (a, %World)의 함수와 같다(비록a는 두 번째 상황에서 선형이지 첫 번째 상황이 아니다).이것은 내가 원하는 것과 매우 가깝지만 약간의 변화가 있다.

우리는 피비린내 나는 세상 전체를 전달하지 않고 캔버스 요소에 대한 WebGL 상하문만 전달할 것이다.

WebGL 함수의 많은 값은 선형이기 때문에 나는 기본적으로 선형 결과와 선형 일원 연산을 사용할 것이다.

결과 데이터 유형:

data GLRes : Type -> Type where
  MkGLRes : (1 result : a) -> (1 gl : AnyPtr) -> GLRes a

GLAction : Type -> Type
GLAction a = (1 gl : AnyPtr) -> GLRes a

export
data GL : (a : Type) -> Type where
  MkGL : (1 _ : GLAction a ) -> GL a

불행하게도, 나는 정말로 GL을 Monad로 바꿀 수 없다. 왜냐하면 Monad는 비선형 유형이 필요하기 때문이다.따라서 인터페이스의 새로운 선형 변형은 다음과 같습니다.

public export
interface LFunctor f where
  map : (1 m : (1 _ : a) -> b) -> (1 _ : f a) -> f b

public export
interface LFunctor f => LApplicative f where
  pure  : (1 _ : a) -> f a
  (<*>) : (1 _ : f ((1 _ : a) -> b)) -> (1 _ : f a) -> f b

public export
interface LApplicative m => LMonad m where
  (>>=)  : (1 _ : m a) -> (1 _ : (1 _ : a) -> m b) -> m b

이것은 Idris에서 매우 효과적이다. 왜냐하면 도 기호는 bind(>>= 조작부호의 문법 설탕일 뿐이지, 토론한 유형이 Monad의 실례가 아니기 때문이다.

-- LFunctor and LApplicative left out as they were not particularly interesting
export
LMonad GL where
  (>>=) (MkGL action_a) gl_b =
    MkGL $ \gl =>
      let
        MkGLRes result_a gl' = action_a gl
        MkGL action_b = gl_b result_a
      in
        action_b gl'

그리고 나머지는 나의 모든 기능을 조정하고 새로운 GL monad를 다시 사용하는 것이다.GLContext를 선형 유형으로 직접 전달하면 외부 함수는 다음과 같습니다.

%foreign "browser:lambda: (gl, r, g, b, a) => {gl.clearColor(r,g,b,a); return gl;}"
prim__clearColor : (1 _ : AnyPtr) -> Double -> Double -> Double -> Double -> AnyPtr

포장지:

export
clearColor : Double -> Double -> Double -> Double -> GL ()
clearColor r g b a = MkGL $ \gl =>
  let
    gl' = prim__clearColor gl r g b a
  in
    MkGLRes () gl'

일부 함수는 자바스크립트에서 여러 개의 값을 되돌려 주기 때문에 더욱 복잡하다. 그러나 원리는 같다. MkGL 는 gl 를 입력하고 생성하는 GLRes 함수와 함께 사용하고, 그 중 어느 곳에서 기원 함수를 호출한다.
새 GL monad를 사용하는 코드의 모양에 만족합니다.

createShaderFromSource : WebGL2.GLShaderType -> String -> (1 _ : (1 _ : GLShader) -> GL a) -> GL a
createShaderFromSource shaderType shaderSrc p =
  createShader shaderType $ \shader => do
    shader <- shaderSource shader shaderSrc
    shader <- compileShader shader
    p shader

createShaderProgram : String -> String -> (1 _ : (1 _ : WebGL2.GLProgram) -> GL a) -> GL a
createShaderProgram vertexSrc fragmentSrc p =
  createShaderFromSource GL_VERTEX_SHADER vertexSrc $ \vs =>
    createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc $ \fs =>
      createProgram $ \program => do
        (program, vs) <- attachShader program vs
        (program, fs) <- attachShader program fs
        program       <- linkProgram program
        ()            <- deleteShader vs --we need to consume the returned unit because it is linear...
        ()            <- deleteShader fs
        p program

내가 남긴 주요 걱정은 코드의 현재 외관이다.

requestAnimationFrame, 이것은 반드시 이용해야 한다IO (). 왜냐하면 이것은 미래의 어느 때에 함수를 실행하는 것이지 되돌아오는 값이 아니기 때문이다.선형 WebGL 컨텍스트는 "실행"할 수 없습니다.

어느 곳에서든 피비린내 나는 연속이 있어 선형 가치를 창조했다.지금 생각해 봤는데, 나는 GL의 작업 원리를 고려하여, 내가 그것들을 더 필요로 하는지 검사해야 한다.

비싼 분배를 피하기 위해 임시 유형의 그룹을 원합니다.이것은 선형을 통해 실현할 수 있다.사실 이것은 그들 배후의 동기 중의 하나다.나는 GL monad와 유사한 일을 하고 싶지만, 전달할 수 있는 현저한 자원이 없고, '분배기' 대상이 없다.

여기저기 구축GL과GLRes값의 성능 결과가 걱정입니다. Idris는 아직 최적화되지 않았지만(현재) 성능에 뚜렷한 영향을 미치지 않는 것 같습니다.브라우저의 JS 엔진/컴파일러가 이 최적화 절차를 성공적으로 실현했거나, 성능이 CPU의 제한을 받지 않았거나.

선형 유형이 입출력 리스트에 미치는 영향
a post by Conal Elliot에서 농담으로 지적한 바와 같이 IO monad에서 작업은 기본적으로 프로세스 프로그래밍을 하는 것과 같다. 만약에 Idris나Haskell 같은 코드를 작성한다면 이것은 당신이 하고 싶은 것이 아닐 수도 있다.
Idris는 흑마법이 아닌 선형으로 정의하는 IO monad를 개선했습니다.이렇게 하는 과정에서 IO의 약점을 드러냈다. 즉catch-all 유형%World을 사용했다.이것은catch 함수에서 '동적' 형식을 사용하거나 오류와 일치하는 것과 같다.유형 보안과 일치하지 않습니다.
선형 유형이 추가됨에 따라 프로그래머가 자신의 자원을 정의하는 것이 더욱 쉬워졌다. 로그 출력, 인터넷 연결, 고화질 접근.이런 물건을 지정하는 것이 더 안전하고,monad transformers 심지어free(r)monad를 사용하여 그것들을 조합할 수 있습니다.만약 조작의 밑바닥 자원이 존재하지 않거나 이 자원을 직접 인용할 수 없다면 (유형화 수조 분배와 마찬가지로) 위조 자원, 즉 단원의 추상적인 데이터 형식을 사용할 수 있다.우리는 입출력 리스트에 대한 의존을 효과적으로 끝낼 수 있다.그래서 나는 전주곡이나 기본곡에 모두 수배IO나%World가 있어야 한다고 생각하지 않는다. 왜냐하면 나는 지금 그것들이 반모드라고 생각할 수밖에 없기 때문이다.
만약 우리가 제거IO한다면 아직도 해결해야 할 문제가 좀 있다. 나는 내가 이 문제들을 모두 모른다고 믿는다.우선, 때로는 일이 사실상 운행만 하고 있을 때도 있다.상술한 requestAnimationFrame 예가 바로 이런 상황이다.그러나 FFI에 특정한 해결 방안이 필요한 FFI 문제로 분류해야 할지도 모른다.
우리가 현재 IO 리스트로 표현하고 있는 것들은 리스트가 아닐 수도 있습니다.비결정론이 좋은 예다.현재 우리가 랜덤표나 유사한 확정적 기교에 의존하지 않고 위조 랜덤수를 생성한다고 가정하면 비확정적 조작은 고유한 순서가 없기 때문에 단자 강제 조작을 사용하는 것은 가능하지만 정확하지 않다.