Agda是一种很好的编程语言,可以探索依赖类型并使用直觉类型理论并尝试实现这些东西.但是,已经有用Agda编写的"真实"程序的例子吗？也许甚至可以展示其功能的例子(类似于xmonad经常被提到作为"真正的"Haskell程序的一个例子)？
我最近发现了这个git worktree命令:
新的工作目录链接到当前存储库,共享除工作目录特定文件(如HEAD,索引等)之外的所有内容.
但是文档也表明了这一点
...对子模块的支持不完整.建议不要对超级项目进行多次检出.
没有进一步解释什么是错误的.
有人可以告诉我有关预期的问题吗？例如,如果我使用以这种方式生成的单独工作树仅用于不影响子模块的更改,我会没事吗？
我刚刚开始玩Haskell ...我想写一个相同类型的身份的函数.显然,不等于它.那会是这样的,
myfunction :: a -> a
我无法想出一个示例,其中参数和返回类型是相同的,几乎可以是任何东西(这排除了使用Haskell的类型类的可能性).
要获取n列表的最后一个元素xs,我可以使用reverse (take n (reverse xs)),但这不是很好的代码(它在返回任何内容之前将完整列表保留在内存中,并且结果不与原始列表共享).
如何lastR在Haskell中实现此功能？
Haskell编程语言有一个概念newtypes:如果我写newtype Foo = Foo (Bar),那么Foo创建一个同构的新类型Bar,即两者之间存在双射转换.这个结构的属性是:
还有哪些编程语言提供此功能？
当与记录访问器/构造器一起使用时,一个示例似乎是C中的单值结构.当与强制转换一起使用时,无效候选者将是C中的单值结构,因为编译器不会检查强制转换,或者Java中具有单个成员的对象,因为它们不会共享相同的表示.
相关问题:F#是否具有Haskell的"新类型"？(不)D是否有'newtype'？(不再).
haskell programming-languages functional-programming newtype
最初由Launchbury和Peyton Jones设计的ST monad允许Haskell程序员编写命令式代码(使用可变变量,数组等),同时获得该代码的纯接口.
更具体地说,入口点函数的多态类型
runST :: (forall s. ST s a) -> a
确保ST包含计算的所有副作用,并且结果值是纯的.
这是否经过严格(甚至正式)证明？
对于某些类型,一些Haskell仿函数F a显然是同构的,例如T -> aT
data Pair a = Pair a a -- isomorphic to Bool -> a
data Reader r a = Reader (r -> a) -- isomorphic to r -> a (duh!)
data Identity a = Identity a -- isomorphic to () -> a
data Phantom a = Phantom -- isomorphic to void -> a
(这些同构只能达到严格,只考虑有限的数据结构.)
所以一般来说,我们如何在可能的情况下描述仿函数？
问题是"哪个Haskell Functors可以表示？"同样的问题？
我正在玩类型对齐的序列,特别是我正在搞乱折叠它们的想法.可折叠的类型对齐序列看起来像这样:
class FoldableTA fm where
foldMapTA :: Category h =>
(forall b c . a b c -> h b c) ->
fm a b d -> h b d
foldrTA :: (forall b c d . a c d -> h b c -> h b d) ->
h p q -> fm a q r -> h p r
foldlTA :: ...
通过首先使用以天真的方式将序列转换为类型对齐的列表(即,使用类型对齐的列表类别)然后折叠该列表,实现foldrTA起来非常容易.不幸的是,这可能是非常低效的,因为长列表可以预先设置为短列表.我一直试图找出一种方法来使用类似于用于更有效地定义右和左折叠的技巧,但这些类型让我头晕目眩.这似乎不够通用,我从其他方向采取的每一步都会让我得到更多的类型变量,而不是我能追踪到的.foldMapTAfoldMapTAData.FoldableEndo