haskell - 如何制作有限制的类型

Question

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

我怎么做？除了使用 just (x, y)since 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
-}

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

Answer 3

执行此操作的正常依赖类型方法是使用 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 4

只是详细说明 ivanm 的回答：

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 5

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