Например, я хочу создать тип 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
Я думаю, что трюк здесь в том, что вы не применяете его на уровне уровня, вы используете "умные конструкторы": т.е. разрешать создание таких "кортежей" через функцию, которая генерирует такие значения:
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" ), но имеет смысл, чем пытаться иметь какое-то принудительное ограничение на уровне типа для допустимых значений.
Типы могут гарантировать правильный "тип" значения (каламбур не предназначен); чтобы гарантировать достоверность значений, которые вы скрываете конструктора, и разрешать создание только через утвержденные функции, гарантирующие любые требуемые инварианты.
Да, умные конструкторы или 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
-}
И бам, у вас есть статически проверенный инвариант в вашем коде! Кроме того, вы можете лгать...
Нормальным образом типизированный способ сделать это будет использовать тип сигма (зависимый продукт), например, в 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
Вот почему Σ часто называют "экзистенциальным типом": он позволяет указать как некоторые данные, так и некоторое свойство об этих данных.
Я не эксперт в этом, но я не думаю, что вы можете реализовать это в Haskell на уровне уровня, так как Haskell не поддерживает зависимые типы. Возможно, вы захотите посмотреть на Агду.
Просто проработав на 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