如何制作有限制的类型

Question

例如，我想创建一个整数三元组类型MyType。但不仅仅是三个整数的笛卡尔积，我希望该类型代表所有 (x, y, z)，例如 x + y + z = 5。

我该怎么做？除了只使用(x, y)，因为z = 5 - x - y。

如果我有三个构造函数 A, B, C 并且类型应该都是 (A x, B y, C z) 这样x + y + z = 5，那么同样的问题。

Answer 1

仅详细说明 ivanm 的 answer：

data MyType = MT {x :: Int, y :: Int, z :: Int } deriving Show

createMyType :: Int -> Int -> Int -> Maybe MyType
createMyType a b c
    | a + b + c == 5 = Just MT { x = a, y = b, z = c }
    | otherwise      = Nothing

Answer 2

执行此操作的正常依赖类型方法是使用 sigma（依赖产品）类型，例如在 Agda 中：

open import Relation.Binary.PropositionalEquality (_≡_)
open import Data.Nat (ℕ; _+_)
open import Data.Product (Σ; ×; _,_)

FiveTriple : Set
FiveTriple = Σ (ℕ × ℕ × ℕ) (λ{ (x , y , z) → x + y + z ≡ 5 })

someFiveTriple : FiveTriple
someFiveTriple = (0 , 2 , 5) , refl

这就是为什么 Σ 通常被称为“存在”类型：它允许您指定一些数据和关于该数据的一些属性。

Answer 3

是的，智能构造函数或 Agda 是这里的最佳选择，但如果你真的想疯狂地使用 Haskell 中的“依赖”方法：

{-# LANGUAGE GADTs, TypeFamilies, RankNTypes, StandaloneDeriving, UndecidableInstances, TypeOperators #-}

data Z = Z
data S n = S n

data Nat n where
  Zero :: Nat Z
  Suc  :: Nat n -> Nat (S n)

deriving instance Show (Nat n)

type family (:+) a b :: *
type instance (:+) Z b = b
type instance (:+) (S a) b = S (a :+ b)

plus :: Nat x -> Nat y -> Nat (x :+ y)
plus Zero y = y
plus (Suc x) y = Suc (x `plus` y)

type family (:*) a b :: *
type instance (:*) Z b = Z
type instance (:*) (S a) b = b :+ (a :* b)

times :: Nat x -> Nat y -> Nat (x :* y)
times Zero y = Zero
times (Suc x) y = y `plus` (x `times` y)

data (:==) a b where
  Refl :: a :== a

deriving instance Show (a :== b)

cong :: a :== b -> f a :== f b
cong Refl = Refl

data Triple where
  Triple :: Nat x -> Nat y -> Nat z -> (z :== (x :+ y)) -> Triple

deriving instance Show Triple

-- Half a decision procedure
equal :: Nat x -> Nat y -> Maybe (x :== y)
equal Zero Zero = Just Refl
equal (Suc x) Zero = Nothing
equal Zero (Suc y) = Nothing
equal (Suc x) (Suc y) = cong `fmap` equal x y

triple' :: Nat x -> Nat y -> Nat z -> Maybe Triple
triple' x y z = fmap (Triple x y z) $ equal z (x `plus` y)

toNat :: (forall n. Nat n -> r) -> Integer -> r
toNat f n | n < 0 = error "why can't we have a natural type?"
toNat f 0 = f Zero
toNat f n = toNat (f . Suc) (n - 1)

triple :: Integer -> Integer -> Integer -> Maybe Triple
triple x y z = toNat (\x' -> toNat (\y' -> toNat (\z' -> triple' x' y' z') z) y) x

data Yatima where
  Yatima :: Nat x -> Nat y -> Nat z -> ((x :* x) :+ (y :* y) :+ (z :* z) :== S (S (S (S (S Z))))) -> Yatima

deriving instance Show Yatima

yatima' :: Nat x -> Nat y -> Nat z -> Maybe Yatima
yatima' x y z = 
  fmap (Yatima x y z) $ equal ((x `times` x) `plus` (y `times` y) `plus` (z `times` z)) (Suc (Suc (Suc (Suc (Suc Zero)))))

yatima :: Integer -> Integer -> Integer -> Maybe Yatima
yatima x y z = toNat (\x' -> toNat (\y' -> toNat (\z' -> yatima' x' y' z') z) y) x


{-
λ> triple 3 4 5
Nothing
λ> triple 3 4 7
Just (Triple (Suc (Suc (Suc Zero))) (Suc (Suc (Suc (Suc Zero)))) Refl (Suc (Suc (Suc (Suc (Suc (Suc (Suc Zero))))))))

λ> yatima 0 1 2 
Just (Yatima Zero (Suc Zero) (Suc (Suc Zero)) Refl)
λ> yatima 1 1 2 
Nothing
-}

然后，您的代码中有一个静态检查的不变量！除非你可以撒谎......

Answer 4

我不是这方面的专家，但我认为你不能在 Haskell 中的类型级别实现这一点，因为 Haskell 不支持依赖类型。你可能想看看 Agda。

Answer 5

我认为这里的诀窍是您不在类型级别强制执行它，而是使用“智能构造函数”：即只允许通过生成此类值的函数创建此类“元组”：

module Test(MyType,x,y,z,createMyType) where

data MyType = MT { x :: Int, y :: Int, z :: Int }

createMyType :: Int -> Int -> MyType
createMyType myX myY = MT { x = myX, y = myY, z = 5 - myX - myY }

如果您想生成所有可能的此类值，那么您可以编写一个函数来执行此操作，可以使用提供的或指定的边界。

很可能使用类型级别的教堂数字或类似的东西来强制创建这些数字，但对于您可能想要/需要的东西来说，这几乎肯定是太多的工作。

这可能不是你想要的（即“除了使用 (x, y)，因为 z = 5 - x - y”），但它比试图对类型级别进行某种强制限制更有意义用于允许有效值。

类型可以确保值的正确“类型”（没有双关语）；为了确保值的有效性，您隐藏了构造函数，并且只允许通过保证您需要的任何不变量的批准函数进行创建。