JAPANESE
依存型
いぞんがた
KOREAN
의존 타입
[ウィジョン タイプ]
ハングル読み: 이존가타
解説
値に依存して型が決まる高度な型システム。配列の長さや数値の範囲を型レベルで表現でき、コンパイル時に境界チェックやビジネスルールの妥当性を検証する。IdrisやAgdaで使用される。
값에 의존하여 타입이 결정되는 고급 타입 시스템이다. 배열의 길이나 수치의 범위를 타입 수준에서 표현할 수 있으며 컴파일 시 경계 체크나 비즈니스 규칙의 타당성을 검증한다. Idris나 Agda에서 사용된다.
例文
依存型で固定長ベクトルの長さを型パラメータとして表現し、範囲外アクセスをコンパイル時に排除した。
의존 타입으로 고정 길이 벡터의 길이를 타입 파라미터로 표현하여 범위 외 접근을 컴파일 시에 배제했다.