Как сделать шрифт с ограничениями

Question

Например, я хочу сделать тип MyType целых троек.Но не только декартово произведение трех целых чисел, я хочу, чтобы тип представлял все (x, y, z) так, чтобы x + y + z = 5

Как мне это сделать?За исключением использования just (x, y), поскольку z = 5 - x - y

И тот же вопрос, если у меня есть три конструктора A, B, C и тип должен быть всем (A x, B y,С 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 }

Если вы хотите сгенерировать все возможные такие значения, то вы можете написать для этого функцию с заданными или указанными границами.

Вполне возможно, можно использовать церковь уровня типаЦифры или что-то подобное для обеспечения их создания, но это почти определенно слишком много работы для того, что вы, вероятно, хотите / нуждаетесь.

Это может быть не то, что вы хотите (т. Е. «За исключением использования just (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

Обычный способ сделать это с зависимой типизацией - использовать сигма-тип (зависимый продукт), например, в 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

Просто уточняю ответ Ивана :

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 не поддерживает зависимые типы. Возможно, вы захотите взглянуть на Агду.