我想有一个归纳类型来描述排列及其对某些容器的行为.很明显,根据这种类型的描述,算法的定义复杂度(就其长度而言)(计算组合或逆,分解成不相交的循环等)将会变化.
考虑Coq中的以下定义.我认为这是Lehmer代码的形式化:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
很容易在大小为n的向量上定义它的动作,在其他容器上稍微硬一些,并且(至少对我而言)很难找到组合的形式化或逆向.
或者,我们可以将置换表示为具有属性的有限映射.可以容易地定义组合或逆,但是将其分解成不相交的循环是困难的.
所以我的问题是:是否有任何文件可以解决这个权衡问题？我设法找到的所有工作都处理了命令式设置中的计算复杂性,而我对"推理复杂性"和函数式编程感兴趣.
在Ralf Hinze的" Kan Extensions for Program Optimization "中,有一个List类型的定义,基于monoid类别中遗忘函子的右Kan延伸(第7.4节).本文给出了Haskell实现如下:
newtype List a = Abstr {
apply :: forall z . (Monoid z) => (a -> z) -> z
}
我能够定义通常的nil和cons构造函数:
nil :: List a
nil = Abstr (\f -> mempty)
cons :: a -> List a -> List a
cons x (Abstr app) = Abstr (\f -> mappend (f x) (app f))
使用以下为Maybe functor的Monoid类实例,我设法定义了head函数:
instance Monoid (Maybe a) where
mempty = Nothing
mappend Nothing m = m
mappend (Just a) m …你能否告诉我有没有为Enum类提供Haskell派生机制的扩展？我的意思是除了"nullary constructors"之外还有很多合理的情况.这个主题有什么作品吗？
我们A, B, C是类型,有两个功能f :: (A , B) -> A和g :: (A , B) -> B.考虑以下记录类型
data Rec = Rec{_a :: A, _b :: B, _c :: C}.
定义映射(Rec a b c)到(Rec (f a b) (g a b) c)使用lens组合器的函数的最优雅方法是什么？