Idris2+WebGL, 제9부분: 제복이 귀속계획에 속하는지 확인

변수 데이터를 셰이더에 전달하기 위해 WebGL/OpenGL은 유니폼과 속성을 사용합니다.그것들을 사용하려면, 프로그램의 제복 위치를 이름으로 가져와야 하고, 우리가 넣고 싶은 데이터로 이 위치를 전달해야 한다.
관련 C 함수는 다음과 같습니다(WebGL 변형과 유사).

GLint glGetUniformLocation(
  GLuint program,
  const GLchar *name
);

void glUniform1fv(
  GLint location,
  GLsizei count,
  const GLfloat *value
);

위치는 하나의 정수일 뿐이며, 서로 다른 프로그램은 서로 다른 일에 대해 같은 위치를 사용할 수 있다.제복을 한 프로그램에서 다른 프로그램으로 전달하는 것은 잘못된 것이지만, 우리가 이렇게 하는 것을 막을 수 있는 것은 아무것도 없다.나는 이 오류를 피하기 위해 유형을 사용하고 싶다. 이것은 상당히 큰 도전이 될 것이다.
효율적인 웹GL 응용 프로그램은 한 번에 여러 개의 통일을 전달하고 프로그램 간에 통일을 유지하는 것을 허용하기 때문에 더욱 복잡한 것 같아서 내가 그곳에 도착했을 때 이 다리를 뛰어넘을 것이다.
이 문제는 두 가지 방면이 있다.우선, 우리는 하나의 통일된 위치가 어떤 착색기 프로그램에 속한다는 것을 표시해야 한다.그 다음으로 현재 귀속된 프로그램을 추적하는 방법이 필요합니다. uniform 함수에 전달된 위치가 현재 귀속된 프로그램에 속하는지 확인할 수 있습니다.운행시 검사를 멀리하고 싶습니다.실행할 때 검사는 비용을 증가시킬 수 있으며, 이 함수들은 관건적인 순환에서 호출되기 때문에 가능한 한 효율적이어야 한다.
이전에 Haskell에서 OpenGL 유형 보안을 실현해 본 적이 있습니다.이 기능, 특히 현재 연결된 프로그램을 추적하는 것은 나로 하여금 포기하게 했다.정확한 원인은 본문에서 더욱 명확해질 것이다.

프로그램에 위치 바인딩

존재 유형
Haskell에서 이 기능을 실현하려고 할 때, 나는 존재 유형을 사용하여 위치를 특정 프로그램과 연결시키기로 결정했다.비교적 높은 차원에서 나는 환영 유형(유형 차원에만 존재하는 유형)을 프로그램의 매개 변수로 사용한다.glGetUniformLocation 프로그램과 같은 환영 유형의 위치를 생성합니다.그러나 createProgram 환영 유형만 존재하고 그것이 무엇인지만 지정한다.이러한 내부 환상 유형의 프로그램에 값을 제공하는 다른 함수가 없으면 구조 함수도 내보내지 않습니다.따라서 위치와 프로그램의 내부 형식이 일치하면 glGetUniformLocation 에서 와야 합니다.
그럼 우리 아이리스로 어떻게 표현할까요?먼저, 프로그램 및 통합 위치에 환영 유형을 추가합니다.

export
data Program : Type -> ProgramStatus -> Type where
  MkProgram : (1 _ : AnyPtr) -> Program p s

export
data UniformLocation : Type -> Type where
  MkUniformLocation : AnyPtr -> UniformLocation p

그리고 적응이 필요해createProgram.내가 아는 바에 의하면, 우리는 존재 유형을 직접 지정할 수 없다.그러나 적극적인 위치에 있는 존재 유형은 소극적인 위치에 있는 보편적인 유형과 같다.또는 더 간단하게 말하자면, 만약 우리가 아는 것이 단지 어떤 사물의 존재일 뿐이라면, 우리는 그것을 모든 사물을 처리하는 함수에 적용할 수 있을 뿐이다.코드:

createProgram : HasGL gl => (forall p . Program p Unlinked -> gl a) -> gl a

또는 공통 양사를 구조 함수에서 음수 위치에 배치하는 새 유형을 만들 수 있습니다.

data ProgramCont : Type -> Type where
  WithProgram : ((forall p . (Program' p s -> a)) -> a) -> ProgramCont s

createProgram : HasGL gl => gl ProgramCont Unlinked

프로그램과 위치 간의 관계를 데이터 유형에 저장할 수 있습니다.

data ProgramLocationPair : Type where
  MkPLP : Program' p Linked -> UniformLocation' p -> ProgramLocationPair

의존형 사기?
상술한 방법은 두 가지 결점이 있다.우선, 나는 단지 계속하는 것을 좋아하지 않을 뿐이다.하나의 존재 유형은 수학적으로 하나의 보편적인 유형의 역수와 같을 수 있지만 양자가 표현하는 사상은 결코 같지 않다.나도 추가로 축소하는 것을 좋아하지 않는다.이것은 인위적인 복잡성이다.
그 다음으로 우리는 추상적인 데이터 형식만을 통해 유형 안전을 실현했다.내보내는 작업이 고장 상태를 초래하지 않기 때문에 안전하다는 것이다.이것은 추적하기 매우 어려운 일이다.
아마도 Idris의 의존 유형을 사용하면 뭔가를 할 수 있을 것이다. 나는 그것들에 대해 아직 익숙하지 않아서 확실하지는 않지만, 나는 그렇게 생각하지 않는다.실행 시간 값을 사용하고 싶지 않기 때문에, 비용을 피하기 위해서, 지난번 로그 항목의 DPair와 같은 구조는 불가능합니다.다른 한편, 컴파일할 때 값은 유형이라고 생각합니다. 같은 코드의 여러 번 호출 사이에 변화가 없기 때문에 우리는 유형의 지식에 의존할 수 없고 무지에만 의존할 수 있습니다.그러나 나는 이 방면에 초보이기 때문에 나의 추리는 잘못된 것일 수도 있다.
내가 할 수 있는 일은 어떤 위치가 프로그램에 속한다는 것을 증명하는 증명 데이터 형식을 만드는 것이다.

data LocationInProgram : Location -> Program -> Type
  MkLocationInProgram : LocationInProgram l p

getUniformLocation를 통해 증거를 되돌려줍니다.그러나 나는 이런 방법이 선형 유형에 잘 쓰일 것이라고 상상할 수 없다.

바인딩 추적
OpenGL 4에는 특정 프로그램의 통일된 위치를 설정하는 함수가 있지만, WebGL은 현재 사용 중인 프로그램에서 통일된 위치를 설정하는 함수만 있다.만약 내가 이 분야에서 유형 안전을 실현하고 싶다면, 나는 어떤 방식으로 프로그램의 연결을 추적해야 한다.

선형도
프로그램이 선형이기 때문에 'is use' 를 환영 형식으로 추가할 수 있습니다.useProgram 두 프로그램 간에 사용 중인 내부 환영 유형을 교환합니다.예를 들면 다음과 같습니다.

useProgram : HasGL gl =>
  (1 _ : Program p1 Linked InUse) ->
  (1 _ : Program p2 Linked NotInUse) ->
  gl (LPair (Program p1 Linked NotInUse) (Program p2 Linked InUse))

그리고 나는 이 프로그램을 통해 통일 함수의 증명으로 삼아야 한다.

uniform1fv : HasGL gl => (1 _ : Program p Linked InUse) -> UniformLocation p -> (1 _ : Float32Array 1) -> Int -> Int -> gl (LPair (Float32Array 1, Program p Linked InUse))

그러나 프로그램이 사용하지 않는 것은 충분히 가능하다. 이것은 사실상 초기 상태이다.이것에 대해 받아들일 수 있는 해결 방법이 있을 수 있습니다. 예를 들어 특수한 'null' 프로그램이 있는데, 이것은 최초의 WebGL 규범에서 함수 호출을 바꾸는 것을 좋아하지 않습니다.이것 또한 이상한 상황을 초래했다. 우리는 지우기와 선형을 동시에 사용하고 싶다. 왜냐하면 우리는 실제로 실행할 때 프로그램을 전달하고 싶지 않기 때문이다.
사용 중인 프로그램의 증인만 전달할 수도 있다.

useProgram : HasGL gl =>
  (1 _ : ProgramWitness p1) ->
  (1 _ : Program p2 Linked) ->
  gl (LPair (ProgramWitness p2) (Program p2 Linked))

그러나 전체적으로 말하자면 이것도 같은 문제가 있다. 비록 유형이 하나의 단원일 수 있지만 스마트 컴파일러는 이를 최적화할 수 있다.Idris JS 백엔드 컴파일러는 아직 그렇게 스마트하지 않다.나도 프로그래머에게 각종 상태 증인을 추적하도록 강요하고 싶지 않다.

국가 명세서
사용 상태 리스트는 그것들의 값만 바꿀 수 있기 때문에 실행할 때 검사해야 하기 때문에 나는 그것들을 고려하지 않는다.

색인 목록
Haskell에서 연결된 프로그램을 추적하려고 할 때 색인 상태 목록을 선택했습니다.이것들은 기본적으로 모두 상태 리스트이기 때문에 상태의 유형이 다를 수 있다.색인 목록은 일반 목록의 '값' 형식을 제외하고 두 가지 형식 변수가 있습니다. 입력 상태 형식과 출력 상태 형식입니다. 이것은 '색인' 을 구성합니다.만약 첫 번째 쪽지의 출력 인덱스가 두 번째 쪽지의 입력 인덱스와 일치한다면, 우리는 두 개의 인덱스 쪽지를 합성할 수 있을 뿐이다.
이것은 나의 하스켈 비밀번호이다.

-- | Indexed counterpart of the functor
class IxFunctor k f | f -> k where
  -- | Indexed variant of @`Data.Functor.fmap`@, retains the indices of the
  -- input IxMonad
  imap :: forall (s1 :: k) (s2 :: k) a b . (a -> b) -> f s1 s2 a -> f s1 s2 b


-- | Indexed monad m with index kind k
class IxFunctor k m => IxMonad k m | m -> k where
  -- | indexed variant of the @`Control.Monad.return`@ function, does not alter
  -- the index
  return :: forall (s :: k) a . a -> m s s a
  -- | indexed variant of the bind operator @`Control.Monad.>>=`@.
  (>>=) :: forall (s1 :: k) (s2 :: k) (s3 :: k) a b. m s1 s2 a -> (a -> m s2 s3 b) -> m s1 s3 b
  -- | indexed variant of the @`Control.Monad.>>`@ operator.
  (>>) :: forall (s1 :: k) (s2 :: k) (s3 :: k) a b . m s1 s2 a -> m s2 s3 b -> m s1 s3 b
  (>>) v w = v >>= \_ -> w

이런 방법의 문제는 지수가 정확한 상태를 가지고 있다는 데 있다.나는 지식을 대표하고 싶다.지식은 잊혀질 수 있고, 정확한 상태는 수동으로 바뀌어야 한다.때때로 우리는 순환이 끝날 때 어떤 프로그램을 연결했는지 모를 뿐, 개의치 않는다.색인 리스트에 대해 프로그래머는 반드시 현식 호출 forgetProgram 함수를 사용해야 하는데, 이것은 좀 얄밉다.

지식 목록
나는 여전히 이것이 가능한지 확실하지 않지만, 색인 리스트 이후에, 나는 지식을 정확한 상태가 아니라 지식으로 표시하고, 서로 다른 귀속 조작 규칙을 사용하려고 한다.솔직히 나는 세부 사항을 기억하지 못하지만 결과적으로 여러 개의'지식 리스트'를 연결한 후 입력 유형과 출력 유형 사이에 여러 개의'경로'가 존재한다.컴파일러는 이런 불확실성을 조금도 좋아하지 않는다.
나는 이 실험을 반복하는 것에 그다지 흥미가 없다. 왜냐하면 그것은 상당히 복잡하기 때문에, Idris 컴파일러가 그것을 더 좋아할지 확실하지 않다.

홀 리스트
내가 하고 싶은 것은 기본적으로 홀 논리이기 때문에 나는 인터넷에서 기능 상하문에서 이 점을 실현하는 방법을 검색하고 하나를 찾았다article about the Hoare state monad.해결 방안은 Coq에서 Haskell에서 실현할 수 없는 것으로 알고 있습니다.Idris에서 이 점을 어떻게 표현할 수 있는지, 색인 목록의 완전한 정의 상태 유형 문제를 돌아갈 수 있는지, 그리고 이렇게 하면 실행 비용을 초래할 수 있는지를 연구하고 있습니다.

요컨대
머리가 아파요.