如何制作有限制的类型

Question

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

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

同样的问题,如果我有三个构造函数A,B,C和类型应该是所有(A x,B y,C z),使得x + y + z = 5

Answer 1

我认为这里的技巧是你没有在类型级别强制执行它,你使用"智能构造函数":即只允许通过生成这样的值的函数创建这样的"元组":

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")但是它比在类型级别上设置某种强制限制以允许有效更有意义值.

类型可以确保正确的"类型"价值(没有双关语); 确保隐藏构造函数的值的有效性,并且只允许通过批准的函数创建,以保证您需要的任何不变量.

Answer 2

是的,聪明的构造函数或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
-}

而且,你的代码中有一个静态检查的不变量!除了你可以骗...