小编Sjo*_*her的帖子

我有这段代码:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, GADTs, FlexibleInstances, FlexibleContexts #-}

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin …

我想有一个归纳类型来描述排列及其对某些容器的行为.很明显,根据这种类型的描述,算法的定义复杂度(就其长度而言)(计算组合或逆,分解成不相交的循环等)将会变化.

考虑Coq中的以下定义.我认为这是Lehmer代码的形式化:

Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).

很容易在大小为n的向量上定义它的动作,在其他容器上稍微硬一些,并且(至少对我而言)很难找到组合的形式化或逆向.

或者,我们可以将置换表示为具有属性的有限映射.可以容易地定义组合或逆,但是将其分解成不相交的循环是困难的.

所以我的问题是:是否有任何文件可以解决这个权衡问题？我设法找到的所有工作都处理了命令式设置中的计算复杂性,而我对"推理复杂性"和函数式编程感兴趣.

好吧,我正在研究Haskell Monads.当我阅读Wikibook 类别理论文章时,我发现monad态射的签名看起来很像逻辑中的重言式,但你需要转换M a为~~A,这里~是逻辑否定.

return :: a -> M a -- Map to tautology A => ~~A, double negation introduction
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B

其他业务也是重言式:

fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B)
join :: M (M a) -> M a …

import Prelude hiding (foldr)

import Control.Applicative
import Data.Foldable
import Data.Traversable

left, right :: (Applicative f, Traversable t) => (a -> b -> b) -> b -> t (f a) -> f b
left f z = fmap (foldr f z) . sequenceA
right f z = foldr (liftA2 f) (pure z)

我强烈怀疑左右表达是否相等,但如何证明呢？

heist :: (Num n) => [n] -> [n] -> n -> n
-- heist [] [] _ = 0
heist w v maxw = func w v i j where
    i = length w
    j = maxw  
func :: (Num n) => [n] -> [n] -> n -> n -> n 
func _ _ 0 0 = 0

上面的代码给了我:

Heist.hs:15:27:
    Could not deduce (n ~ Int)
    from the context (Num n)
      bound by the type signature for
                 heist :: Num …