용기(유형 이론)

Container (type theory)

형식 이론에서 용기는 목록과 나무와 같은 다양한 "수집 유형"이 균일하게 표현될 수 있도록 하는 추상화다. (단일) 용기는 형상 S의 유형과 위치 P의 유형으로 정의되며, S에 의해 색인화된다. 컨테이너의 확장은 (S형식의) 형태와 그 형태의 위치에서 요소 유형까지의 함수로 구성된 종속 쌍의 제품군이다. 컨테이너는 수집 유형에 대한 표준적인 형태로 볼 수 있다.[1]

리스트의 경우 모양 유형은 자연수(0을 포함)이다. 해당 위치 유형은 각 모양에 대해 형상보다 작은 자연수 유형이다.

나무의 경우 형태형은 단위 나무의 유형(즉, 그 안에 정보가 없는 나무, 단지 구조만 있는 나무)이다. 해당 위치 유형은 각 모양에 대해 모양상의 루트부터 특정 노드까지의 유효 경로 유형에 대해 이형성이 있다.

자연수는 단위 목록과 이형성이라는 점에 유의하십시오. 일반적으로 형상 유형은 장치에 적용되는 원래 비일반 용기 유형 패밀리(목록, 트리 등)와 항상 이형성이어야 한다.

컨테이너의 개념을 도입하는 주된 동기 중 하나는 의존적으로 입력된 환경에서 일반적인 프로그래밍을 지원하는 것이다.[1]

범주적 측면

용기의 연장은 내분자(endofunctor. 그것은 기능을 필요로 한다. g 로

이것은 친숙한 것과 같다. map g 리스트의 경우, 그리고 다른 용기에 대해서도 비슷한 일을 한다.

인덱싱된 컨테이너

인덱싱된 용기(종속적인 다항식 functor라고도 함)는 용기의 일반화로서 벡터(크기 목록)와 같은 더 넓은 종류의 유형을 나타낼 수 있다.[2]

원소형(입력형이라고 함)은 형태와 위치에 따라 인덱싱되기 때문에 모양과 위치에 따라 다를 수 있으며, 확장형(출력형이라고 함)도 형태에 따라 인덱싱된다.

참고 항목

참조

  1. ^ a b Michael Abbott; Thorsten Altenkirch; Neil Ghani (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 3–27. doi:10.1016/j.tcs.2005.06.002.
  2. ^ Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. "Indexed Containers" (PDF). Unpublished manuscript. Retrieved 2008-10-30. {{cite journal}}: Cite 저널은 필요로 한다. journal= (도움말)CS1 maint: 여러 이름: 작성자 목록(링크)

외부 링크


이 프로그래밍 언어 이론이나 유형 이론 관련 기사는 단조롭다. 위키피디아를 확장하여 도울 수 있다.