blocks|key|802086|text|我认为这里的诀窍是你不在类型级别强制它，你使用“智能构造函数”：即只允许通过生成这样的值的函数来创建这样的“元组”：|type|unstyled|depth|inlineStyleRanges|entityRanges|data|802087|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+}|code-block|syntax|javascript|802088|如果您希望生成所有可能的此类值，则可以编写一个函数来实现此目的，可以使用提供的或指定的界限。|802089|可以很好地使用类型级别的教堂数字或一些类似的数字来强制创建这些数字，但对于您可能想要/需要的内容来说，这几乎肯定是太多的工作。|802090|这可能不是您想要的(即“除了只使用(x，y)，因为z=5-x-+y")，但它比试图在类型级别上强制限制允许有效值更有意义。|802091|类型可以确保值的正确“类型”(没有双关语)；为了确保值的有效性，您可以隐藏构造函数，并且只允许通过经过批准的函数创建，以保证所需的任何不变量。|802092|entityMap^0|0|0|0|0|0|0^^$0|@$1|2|3|4|5|6|7|Q|8|@]|9|@]|A|$]]|$1|B|3|C|5|D|7|R|8|@]|9|@]|A|$E|F]]|$1|G|3|H|5|6|7|S|8|@]|9|@]|A|$]]|$1|I|3|J|5|6|7|T|8|@]|9|@]|A|$]]|$1|K|3|L|5|6|7|U|8|@]|9|@]|A|$]]|$1|M|3|N|5|6|7|V|8|@]|9|@]|A|$]]|$1|O|3|-4|5|6|7|W|8|@]|9|@]|A|$]]]|P|$]]

I think the trick here is that you don't enforce it on the type-level, you use "smart constructors": i.e. only allow creation of such "tuples" via a function that generates such values:

<pre><code>module Test(MyType,x,y,z,createMyType) where

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

createMyType :: Int -&gt; Int -&gt; MyType
createMyType myX myY = MT { x = myX, y = myY, z = 5 - myX - myY }
</code></pre>

If you want to generate all possible such values, then you can write a function to do so, either with provided or specified bounds.

It may very well be possible to use type-level Church Numerals or some such so as to enforce creation of these, but it's almost definitely too much work for what you probably want/need.

This might not be what you want (i.e. "Except of using just (x, y) since z = 5 - x - y") but it makes more sense than trying to have some kind of enforced restriction on the type level for allowing valid values.

Types can ensure the correct "type" of value (no pun intended); to ensure validity of values you hide the constructor and only allow creation via approved functions that guarantee any invariants you require.

blocks|key|805811|text|我不是这方面的专家，但我认为你不能在Haskell的类型级别上实现这一点，因为Haskell不支持依赖类型。你可能想看看Agda。|type|unstyled|depth|inlineStyleRanges|entityRanges|data|805812|entityMap^0|0^^$0|@$1|2|3|4|5|6|7|D|8|@]|9|@]|A|$]]|$1|B|3|-4|5|6|7|E|8|@]|9|@]|A|$]]]|C|$]]

I'm not an expert on this, but I don't think you can implement this in Haskell at the type level, as Haskell does not support dependent types. You might want to look at Agda.

blocks|key|805830|text|是的，智能构造器或Agda在这里是可行的，但如果你真的想疯狂地使用“依赖”方法，在Haskell中：|type|unstyled|depth|inlineStyleRanges|entityRanges|data|805831|{-#+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+(:%2B)+a+b+::+*
type+instance+(:%2B)+Z+b+=+b
type+instance+(:%2B)+(S+a)+b+=+S+(a+:%2B+b)

plus+::+Nat+x+->+Nat+y+->+Nat+(x+:%2B+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+:%2B+(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+:%2B+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+%7C+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)+:%2B+(y+:*+y)+:%2B+(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
-}|code-block|syntax|javascript|805832|然后，你的代码中有一个静态检查的不变量！除了你可以说谎..。|805833|entityMap^0|0|0|0^^$0|@$1|2|3|4|5|6|7|K|8|@]|9|@]|A|$]]|$1|B|3|C|5|D|7|L|8|@]|9|@]|A|$E|F]]|$1|G|3|H|5|6|7|M|8|@]|9|@]|A|$]]|$1|I|3|-4|5|6|7|N|8|@]|9|@]|A|$]]]|J|$]]

Yes, smart constructors or Agda are the way to go here, but if you really wanted to go crazy with the "dependent" approach, in Haskell:

<pre><code>{-# 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 -&gt; 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 -&gt; Nat y -&gt; 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 -&gt; Nat y -&gt; 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 -&gt; f a :== f b
cong Refl = Refl

data Triple where
 Triple :: Nat x -&gt; Nat y -&gt; Nat z -&gt; (z :== (x :+ y)) -&gt; Triple

deriving instance Show Triple

-- Half a decision procedure
equal :: Nat x -&gt; Nat y -&gt; 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 -&gt; Nat y -&gt; Nat z -&gt; Maybe Triple
triple' x y z = fmap (Triple x y z) $ equal z (x `plus` y)

toNat :: (forall n. Nat n -&gt; r) -&gt; Integer -&gt; r
toNat f n | n &lt; 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 -&gt; Integer -&gt; Integer -&gt; Maybe Triple
triple x y z = toNat (\x' -&gt; toNat (\y' -&gt; toNat (\z' -&gt; triple' x' y' z') z) y) x

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

deriving instance Show Yatima

yatima' :: Nat x -&gt; Nat y -&gt; Nat z -&gt; 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 -&gt; Integer -&gt; Integer -&gt; Maybe Yatima
yatima x y z = toNat (\x' -&gt; toNat (\y' -&gt; toNat (\z' -&gt; yatima' x' y' z') z) y) x


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

λ&gt; yatima 0 1 2 
Just (Yatima Zero (Suc Zero) (Suc (Suc Zero)) Refl)
λ&gt; yatima 1 1 2 
Nothing
-}
</code></pre>

And bam, you have a statically checked invariant in your code! Except you can lie...

blocks|key|802130|text|通常的依赖类型方法是使用sigma+(依赖产品)类型，例如在Agda中：|type|unstyled|depth|inlineStyleRanges|entityRanges|data|802131|open+import+Relation.Binary.PropositionalEquality+(_≡_)
open+import+Data.Nat+(ℕ;+_%2B_)
open+import+Data.Product+(Σ;+×;+_,_)

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

someFiveTriple+:+FiveTriple
someFiveTriple+=+(0+,+2+,+5)+,+refl|code-block|syntax|javascript|802132|这就是为什么Σ通常被称为“存在的”类型:它允许您指定某些数据和有关该数据的某些属性。|802133|entityMap^0|0|0|0^^$0|@$1|2|3|4|5|6|7|K|8|@]|9|@]|A|$]]|$1|B|3|C|5|D|7|L|8|@]|9|@]|A|$E|F]]|$1|G|3|H|5|6|7|M|8|@]|9|@]|A|$]]|$1|I|3|-4|5|6|7|N|8|@]|9|@]|A|$]]]|J|$]]

The normal dependently-typed way to do this would be to use a sigma (dependent product) type, for example in Agda:

<pre><code>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
</code></pre>

This is why Σ is often called an ‘existential’ type: it allows you to specify both some data and some property about that data.

blocks|key|4761811|text|我只是在详述ivanm的answer|type|unstyled|depth|inlineStyleRanges|entityRanges|offset|length|data|4761812|data+MyType+=+MT+{x+::+Int,+y+::+Int,+z+::+Int+}+deriving+Show

createMyType+::+Int+->+Int+->+Int+->+Maybe+MyType
createMyType+a+b+c
++++%7C+a+%2B+b+%2B+c+==+5+=+Just+MT+{+x+=+a,+y+=+b,+z+=+c+}
++++%7C+otherwise++++++=+Nothing|code-block|syntax|javascript|4761813|entityMap|0|LINK|mutability|MUTABLE|url|https://stackoverflow.com/a/7978377/21480^0|C|6|0|0|0^^$0|@$1|2|3|4|5|6|7|Q|8|@]|9|@$A|R|B|S|1|T]]|C|$]]|$1|D|3|E|5|F|7|U|8|@]|9|@]|C|$G|H]]|$1|I|3|-4|5|6|7|V|8|@]|9|@]|C|$]]]|J|$K|$5|L|M|N|C|$O|P]]]]

Just elaborating on ivanm's <a href="https://stackoverflow.com/a/7978377/21480">answer</a>:

<pre><code>data MyType = MT {x :: Int, y :: Int, z :: Int } deriving Show

createMyType :: Int -&gt; Int -&gt; Int -&gt; Maybe MyType
createMyType a b c
 | a + b + c == 5 = Just MT { x = a, y = b, z = c }
 | otherwise = Nothing
</code></pre>

For example I want to make a type <code>MyType</code> of integer triples. But not just Cartesian product of three Integer, I want the type to represent all (x, y, z) such that <code>x + y + z = 5</code>.
How do I do that? Except of using just <code>(x, y)</code> since <code>z = 5 - x - y</code>.
And the same question if I have three constructors <code>A, B, C</code> and the type should be all <code>(A x, B y, C z)</code> such that <code>x + y + z = 5</code>.

How to make a type with restrictions

翻译质量差，导致语言生硬或混乱。

没有提供实际的解决方法或示例。

解答不清晰，无法理解或解决问题。

页面排版不美观，阅读体验差。

文章

问答

视频

学习中心

腾讯云实验室

直播

竞赛

腾讯云代码分析专区

腾讯iOA零信任安全管理系统专区

腾讯云架构师技术同盟交流圈

腾讯云数据库专区

腾讯云顾问专区

腾讯云原生专区

腾讯混元专区

腾讯云TCE专区

腾讯云Lighthouse专区

腾讯云HAI专区

腾讯云Edgeone专区

腾讯云存储专区

腾讯云智能专区

腾讯轻联专区 

腾讯云开发专区

TAPD专区

腾讯轻量云游戏服专区

腾讯云最具价值专家

腾讯云架构师技术同盟

腾讯云创作之星

腾讯云开发者先锋

腾讯云代码助手

云原生构建

TAPD 敏捷项目管理

Cloud Studio

SDK中心

API中心

命令行工具

涵盖代码开发、场景应用、自动测试全流程，助你从零构建专属AI助手

一站式MCP教程库，解锁AI应用新玩法

例如，我想创建一个整数三元组的类型MyType。但不只是三个整数的笛卡尔乘积，我希望类型表示所有(x，y，z)，这样x + y + z = 5。我该怎么做？除了从z = 5 - x - y开始只使用(x, y)。同样的问题，如果我有三个构造器A, B, C，类型应该都是(A x, B y, C z)，这样x + y +...

问如何创建带约束的类型
EN

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问如何创建带约束的类型EN