我被证明的一些性质filter和map,一切都相当不错,直到我无意中发现这个属性:filter p (map f xs) ? map f (filter (p ? f) xs).以下是相关代码的一部分:
open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.List hiding (filter)
import Level
filter : ? {a} {A : Set a} ? (A ? Bool) ? List A ? List A
filter _ [] = []
filter p (x ? xs) with p x
... | true = x ? filter p xs
... | false = filter p xs
现在,因为我喜欢用 …
我有两个密切相关的问题:
首先,如何在Agda中对Haskell的Arrow类进行建模/表示？
class Arrow a where
arr :: (b -> c) -> a b c
(>>>) :: a b c -> a c d -> a b d
first :: a b c -> a (b,d) (c,d)
second :: a b c -> a (d,b) (d,c)
(***) :: a b c -> a b' c' -> a (b,b') (c,c')
(&&&) :: a b c -> a b c' -> a b (c,c')
(以下博客文章指出它应该是可能的......)
其次,在Haskell中,它(->)是一流的公民,只是另一个更高阶的类型,它可以直接定义(->)为 …
毋庸置疑,Haskell的标准结构
newtype Fix f = Fix { getFix :: f (Fix f) }
cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . getFix
太棒了,非常有用.
试图在Agda中定义类似的东西(我只是为了完整起见)
data Fix (f : Set -> Set) : Set where
mkFix : f (Fix f) -> Fix f
失败,因为f不一定是严格积极的.这是有道理的 - 通过适当选择,我很容易从这种结构中得到一个矛盾.
我的问题是:在Agda编码递归方案有什么希望吗？它完成了吗？需要什么？
我正在Idris中编写一个基本的monadic解析器,以熟悉Haskell的语法和差异.我有基本的工作正常,但我坚持尝试为解析器创建VerifiedSemigroup和VerifiedMonoid实例.
不用多说,这里是解析器类型,Semigroup和Monoid实例,以及VerifiedSemigroup实例的开始.
data ParserM a = Parser (String -> List (a, String))
parse : ParserM a -> String -> List (a, String)
parse (Parser p) = p
instance Semigroup (ParserM a) where
p <+> q = Parser (\s => parse p s ++ parse q s)
instance Monoid (ParserM a) where
neutral = Parser (const [])
instance VerifiedSemigroup (ParserM a) where
semigroupOpIsAssociative (Parser p) (Parser q) (Parser r) = ?whatGoesHere
我基本上被卡住了intros,具有以下证明状态:
-Parser.whatGoesHere> intros
---------- Other goals: ----------
{hole3},{hole2},{hole1},{hole0} …我试图解析Agda中的嵌套列表.我在谷歌搜索,我发现最接近的是在Haskell中解析,但通常使用像"parsec"这样的库,这些库在Agda中不可用.
所以我想"((1,2,3),(4,5,6))"用结果类型解析(List (List Nat)).
并且应该支持进一步的嵌套列表(直到深度5),例如,深度3将是(List (List (List Nat))).
我的代码非常冗长和繁琐,它只适用于(List (List Nat))但不适用于其他嵌套列表.我自己没有取得任何进展.
如果有帮助,我想splitBy从我的一篇旧帖子的第一个答案中重复使用.
NesList : ? ? Set
NesList 0 = ? -- this case is easy
NesList 1 = List ? -- this case is easy
NesList 2 = List (List ?)
NesList 3 = List (List (List ?))
NesList 4 = List (List (List (List ?)))
NesList 5 = List (List (List (List (List ?)))) -- I …我在看如何inorder + preorder构造独特的二叉树？并认为在伊德里斯写一个正式的证据会很有趣.不幸的是,我得到了相当坚持早,试图证明的方式找到树中的元素对应找到它在其序遍历的方式(当然,我还需要做的序遍历) .任何想法都会受到欢迎.我对完整的解决方案并不特别感兴趣 - 更多的是帮助我们开始正确的方向.
特定
data Tree a = Tip
| Node (Tree a) a (Tree a)
我可以通过至少两种方式将其转换为列表:
inorder : Tree a -> List a
inorder Tip = []
inorder (Node l v r) = inorder l ++ [v] ++ inorder r
要么
foldrTree : (a -> b -> b) -> b -> Tree a -> b
foldrTree c n Tip = n
foldrTree c n (Node l v r) = foldr c (v `c` foldrTree …这个最近的SO问题促使我在Haskell中编写了一个不安全且纯粹的ST monad仿真,这是一个稍微修改过的版本,你可以在下面看到:
{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes #-}
import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)
import Data.List
newtype ST s a = ST (State ([Any], Int) a) deriving (Functor, Applicative, Monad)
newtype STRef s a = STRef Int deriving Show
newSTRef :: a -> ST s (STRef s a)
newSTRef a = ST $ do
(env, i) <- get
put (unsafeCoerce a : env, i + 1)
pure (STRef i)
update :: [a] -> (a -> a) …作为什么是Axiom K的后续行动？,我想知道当你使用Agda --without-k选项时会发生什么.结果不那么强大吗？它是一种不同的语言还是所有以前的程序仍然打字检查？
Agda中有哪些大小的类型？我试图阅读有关MiniAgda的文章,但由于以下几点未能继续:
>和#模式意味着什么？是否有F :: * -> * -> * -> *带操作的类型构造函数的标准名称
return :: x -> F a a x
bind :: F a b x -> (x -> F b c y) -> F a c y
这是第一个参数中的逆变函子和第二个和第三个中的协变函子？特别是,这是否与类别理论中的任何类型构造相对应？
这些行动产生了一个
join :: F a b (F b c x) -> F a c x
使这看起来像某种"endofunctors类别中的类别"的操作,但我不确定如何将其正式化.
编辑:正如志所指出的,这与索引的monad有关:给定一个索引的monad
F' : (* -> *) -> (* -> *)
我们可以使用Atkey构造
data (:=) :: * -> * -> * -> *
V :: x -> (x …