제약 데이터 타입

Question

귀납적 인 정의가 있고 그것을 Haskell에서 데이터 타입으로 정의하고자한다고 가정 해보십시오. 그러나 귀하의 귀납적 정의는 생성 규칙에 '전제 (premisses)'가 특정 구조를 가져야하는 양식의 (많은 귀납적 정의만큼) 것입니다. 예를 들어, 우리는 다음과 같은 정의가 있다고 가정

• x 경우는 심지어 정수, 다음 T x이 무기이다,
• 을 x이 S x이 무기 후, 홀수 인 경우. 지금 T 5 및 S 4를 생성 할 수 있습니다 나는 하스켈의 데이터 유형 (단일로)이 정의하려면

, 내가 분명히

data Weapon = T Int | S Int 

처럼 작성할,이를 위해 작동하지 않습니다 예. 생성자 인수에 제한을 전달하는 자연스러운 방법이 있습니까? 그렇다면 올바른 정의를 내릴 수있는 위의 코드와 비슷한 것을 작성할 수 있습니까? YourModule을 가져올 때 만에, 사용자가 명시 적으로 T 및 S을 만들 수 없습니다 이제

module YourModule (Weapon, smartConstruct) where 

data Weapon = T Int | S Int 

smartConstruct :: Int -> Weapon 
smartConstruct x 
    | even x  = T x 
    | otherwise = S x 

:

Answer 1

당신의 최선의 샷은 사용자 정의 생성자를 명시 적으로 T 및 S를 내보내지만, 허용하지 않는 것입니다 귀하의 smartConstruct 기능.

Answer 2

이것은 Haskelly 비트가 아니지만 예를 들어 더 숙성적입니다. Agda : 귀하의 표현의 해석을 변경하여 건설에 의해 강제되도록하십시오.

이 경우 n :: Int 일 경우 even (2 * n) 및 odd (2 * n + 1)입니다. Int이 너무 큰 경우를 핸드웨이에서 제거하면 Int과 Int 사이에 bijection이 있다고 말할 수 있습니다. 홀수 인 Int과 Int 사이에 또 ​​하나가 있습니다. 그래서를 사용

,이 표현 선택할 수 있습니다

data Weapon = T Int | S Int 

을하고 값 T n 실제로 T (2 * n)을 나타내고 값 S n이 S (2 * n + 1)을 대표하도록 해석을 변경합니다. 따라서 어떤 n :: Int을 선택 하든지 T n은 "T -of-2 * n"값으로 간주되므로 유효합니다.

Answer 3

당신이 Nats를 사용하기를 원한다면, 상당히 진보 된 타입의 마법을 사용해도 괜찮습니다. GHC.TypeLits을 사용할 수 있습니다.

{-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-} 

import GHC.TypeLits 

data Weapon (n :: Nat) where 
    Banana  :: n ~ (2 * m) => Weapon n 
    PointyStick :: n ~ (2 * m + 1) => Weapon n 

banana :: Weapon 2 
banana = Banana 

pointyStick :: Weapon 3 
pointyStick = PointyStick 

잘못된 (홀수/짝수) 숫자로 컴파일되지 않도록 노력하십시오.

편집 : 더 많은 실용적인 방법이 있습니다.