英文:
Haskell function with length-indexed vector and predicate constraint
问题
以下是翻译好的代码部分：
这是一个函数f，它仅接受长度为2的索引向量。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Main where
data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One
data Vec :: Nat -> * -> * where
Nil :: Vec Z a
(:>) :: a -> Vec n a -> Vec (S n) a
f :: (l ~ Two) => Vec l a -> a
f (e :> _) = e
要编写一个仅接受长度大于（或小于）2的列表的函数的最佳方法是：
f :: (Gt l Two) => Vec l a -> a
f (e :> _) = e
英文:
Here is function f that takes only length indexed vector with length exacly 2.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
module Main where
data Nat = Z | S Nat deriving Show
type One = S Z
type Two = S One
data Vec :: Nat -> * -> * where
Nil :: Vec Z a
(:>) :: a -> Vec n a -> Vec (S n) a
f :: (l ~ Two) => Vec l a -> a
f (e :> _) = e
What is the best way to write function which only takes list of length greater (or less) then 2 ?
So something like:
f :: (Gt l Two) => Vec l a -> a
f (e :> _) = e
答案1
得分: 4
以下是您要翻译的代码部分：
你可以使用类型家族来定义自己的 `Gt`。
type Gt :: Nat -> Nat -> Constraint
type family Gt n m where
Gt Z _ = 'True ~ 'False
Gt _ Z = ()
Gt (S n) (S m) = Gt n m
然后，你可以使用约束来编写 f。
f :: (Gt l Two) => Vec l a -> a
f (e :> _) = e
但我不确定这是否比以下方式更好。
f' :: Vec (S (S (S n))) a -> a
f' (e :> _) = e
当然，写 (Gt l Hundred) => ... 比 Vec (S (S (S ....))) a ... 更清晰，但无论如何你仍然需要编写 Hundred。
英文:
You can define your own Gt using type families.
type Gt :: Nat -> Nat -> Constraint
type family Gt n m where
Gt Z _ = 'True ~ 'False
Gt _ Z = ()
Gt (S n) (S m) = Gt n m
Then, you can write f using a constraint.
f :: (Gt l Two) => Vec l a -> a
f (e :> _) = e
But I'm not sure if this is better than this.
f' :: Vec (S (S (S n))) a -> a
f' (e :> _) = e
Of course, it'd be cleaner to write (Gt l Hundred) => ... than Vec (S (S (S ....))) a ..., but you still need to write Hundred anyway.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论