程序员经验分享-hwhale

如何在构造微积分中提取Sigma的第二个元素？

2024-03-12

我尝试这样做：

λ (A : *) ->
λ (B : (A -> *)) ->
λ (t : (∀ (r : *) -> (∀ (x : a) -> (B x) -> r)) -> r) ->
(t (B (t A (λ (x : A) -> λ (y : (B x)) -> x)))
    (λ (x : A) -> λ (y : (B x)) -> y))

请注意，由于该函数返回的值取决于 sigma 本身内部的值，因此我需要提取该值。该代码不会进行检查，因为我相信它无法将从 Sigma 中提取的类型与其内部的类型统一起来。

有什么解决方法吗？


None

本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)

Haskell

functionalprogramming

coq

agda

idris

如何在构造微积分中提取Sigma的第二个元素？ 的相关文章

  • 为什么要使用 Python 进行函数式编程？

    在工作中 我们过去常常以非常标准的面向对象方式来编写 Python 程序 最近 有几个人加入了功能性潮流 他们的代码现在包含更多的 lambda map 和reduce 我知道函数式语言有利于并发性 但是函数式 Python 编程真的有助于

  • 如何在 Haskell 中获得列表的中间位置？

    我刚刚开始使用 Haskel 学习函数式编程 我正在慢慢度过Erik Meijer 在 Channel 9 的讲座 http channel9 msdn com shows Going Deep Lecture Series Erik Me

  • 在 Haskell 中将字节转换为 Int64s/Floats/Doubles

    我正在尝试解析 Haskell 中的二进制文件格式 Apple 的二进制属性列表格式 该格式所需的内容之一是将字节序列视为 a 无符号 1 2 或 4 字节整数 b 有符号 8 字节整数 c 32 位floats d 64 位doubles

  • 如何使用 Haskell 中的 thyme 库从 Int 值创建 UTCTime？

    我有年 月 日 小时和分钟值 所有这些都是类型Int 我怎样才能将它们转换为UTCTime or UniversalTime 需要导入以下内容 import Control Lens import Data Thyme Clock impo

  • Swit 中的函数式编程将数组元素分配到正确的“桶”

    我是函数式编程的新手 我的问题是我有一个主数组和固定数量的 目标 数组 我想根据每个元素的特定值将主数组中的元素分配到正确的结果数组中 我猜测一种方法是使用一个映射函数来遍历主数组元素 确定正确的 目标数组 值 基于某种逻辑 然后将元素添加

  • 使用 nix 在 Mac OS X 上由于“架构 x86_64 的未定义符号”而导致“堆栈构建”失败

    首先是错误消息 stack build Linking Users yuzhao stack setup exe cache x86 64 osx tmp Cabal simple mPHDZzAJ 2 2 0 1 ghc 8 4 4 cl

  • ErrorT 已弃用，但 exceptT 不适合

    我有一个一元计算 在某些时候 由于单子模式匹配 它开始需要 MonadFail 约束 我的简单解决方法是使用以下命令运行它 fmap either error id runErrorT 然而哎呀 Deprecated Use Control

  • Haskell 中的前提条件检查有哪些选项

    这是一个简单的问题 我认为答案很复杂 一个非常常见的编程问题是函数返回某些内容 或者前置条件检查失败 在Java中 我会使用一些抛出异常的断言函数IllegalArgumentException在方法的开头 如下所示 method body

  • 如何让 Show 显示函数名称？

    作为一个让我熟悉 Haskell 的简单练习 在 Youtube 上闲逛并偶然进入美国倒计时游戏节目之后 我想为数字游戏制作一个求解器 你得到 6 个数字 需要将它们与 为了得到给定的结果 到目前为止我所得到的是非常脑死亡的 let ope

  • 为什么 Parsec 的 sepBy 停止并且不解析所有元素？

    我正在尝试解析一些逗号分隔的字符串 该字符串可能包含也可能不包含具有图像尺寸的字符串 例如 hello world 300x300 good bye world 我写了下面的小程序 import Text Parsec import qua

  • 什么样的函数被认为是“可组合的”？

    维基百科文章函数组合 计算机科学 https en wikipedia org wiki Function composition computer science says 就像数学中通常的函数组合一样 每个函数的结果作为下一个函数的参数

  • 为什么 Haskell 的默认字符串实现是一个字符链接列表？

    Haskell 默认值的事实String众所周知 实现在速度和内存方面都效率不高 据我所知 lists一般来说 在 Haskell 中实现为单链表 并且适用于大多数小型 简单数据类型 例如Int 这似乎不是一个好主意 但是对于String这

  • 什么是欣德利米尔纳？

    我遇到过这个词欣德利 米尔纳 我不确定是否理解它的意思 我已阅读以下帖子 史蒂夫 叶格 动态语言的反击 http steve yegge blogspot com 2008 05 dynamic languages strike back

  • 纯函数怎么能做IO呢？

    我最近了解到莫纳德随机数 http hackage haskell org package MonadRandom 0 1 13 docs Control Monad Random Class html t 3aMonadRandom图书馆

  • 在依赖类型的函数式编程语言中，扁平化列表是否更容易？

    在 haskell 中寻找一个可以展平任意深度嵌套列表的函数时 即应用的函数concat递归并在最后一次迭代时停止 使用非嵌套列表 我注意到这需要有一个更灵活的类型系统 因为随着列表深度的变化 输入类型也会变化 确实 有几个 stackov

  • 将 num 的签名键入 double？

    我才刚刚开始为你学习 Haskell 以获得伟大的好处 并且我在类型类方面遇到了一些麻烦 我想创建一个接受任何数字类型并强制其为双精度的函数 我的第一个想法是定义 numToDouble Num gt Double 但我认为这不起作用 因为

  • Haskell，堆栈：找到可执行文件

    我正在寻找类似的东西 stack whereis hasktags where whereis行为或多或少类似于 UNIXwhereis命令 hasktags是这样运行的 stack exec hasktags stack exec whe

  • Haskell 中的分类结构

    Hask通常被认为是一个范畴 其对象是类型 态射是函数 然而 我看到 Conor McBride pigworker 警告不要使用Hask多次 1 https stackoverflow com a 45905082 474311 2 ht

  • 规范化且不可变的数据模型

    Haskell如何解决 规范化不可变数据结构 问题 例如 让我们考虑一个表示前女友 男友的数据结构 data Man Man name String exes Woman data Woman Woman name String exes

  • 以下两个 lambda 函数的空间复杂度

    我正在阅读以下内容 https en wikibooks org wiki Haskell Graph reduction https en wikibooks org wiki Haskell Graph reduction 其内容如下

随机推荐

  • 给定一个数的质因数分解，生成该数的所有因数

    如果您已经对一个数字进行质因数分解 那么获得该数字的所有因数的集合的最简单方法是什么 我知道我可以从 2 循环到 sqrt n 并找到所有可整除的数字 但这似乎效率很低 因为我们已经有了质因数分解 我想它基本上是组合 选择函数的修改版本 但

  • 熊猫 corr() 与 corrwith()

    Pandas 提供两种不同的相关函数的原因是什么 DataFrame corrwith 其他 轴 0 drop False 两个DataFrame对象的行或列之间的相关性成对计算 vs DataFrame corr method pears

  • Jackson 序列化 可选，YAML 为空值

    目前我正在使用YAML工厂 https fasterxml github io jackson dataformats text javadoc yaml 2 11 配置ObjectMapper序列化和反序列化Pojos lt gt YAM

  • 显示片段中的对话框？

    我有一些片段需要显示常规对话框 在这些对话框中 用户可以选择是 否答案 然后片段应该做出相应的行为 现在Fragment类没有onCreateDialog 方法来重写 所以我想我必须在包含的外部实现对话框Activity 没关系 但是接下来

  • 当 url 包含锚点时，获取页面加载时网页滚动条的垂直位置

    我使用 jQuery 的scrollTop 方法来获取页面加载时滚动条的垂直位置 我需要在执行 url 中的锚点后获取此值 例如 url www domainname com foo 我可以使用以下代码 它可以在 Firefox 和 IE

  • iPhone 解锁时 Xcode“设备锁定”

    当我尝试构建并运行时 Xcode 说我的设备已锁定 我看了看我的 iPhone 它根本没有锁定 我该如何解决 我的手机设置为 信任 Mac 但我在 Xcode 6 1 1 中仍然遇到此错误 这对我有用 拔掉设备插头 退出 xcode 打开X

  • 测试示例集属性应等于训练示例集 Rapidminer SVM 的 OR 超集

    I am new to Rapid Miner and using SVM Linear in it My model is as I made Training Example set which consist of 3552 exam

  • 动态 Java 整数/长溢出检查与性能

    这是一个相当理论化的问题 因此虽然该语言是 Java 特有的 但任何通用的解决方案都足够了 假设我想编写一个简单的阶乘函数 long factorial int n handle special cases like negatives e

  • Xamarin 表单更改导航栏的背景颜色

    我正在使用 Xamarin Forms 并尝试更改 iOS 上导航栏的背景颜色 我有一个继承自 NavigationPage 的自定义导航栏类 具有可绑定属性和构造函数 用于设置导航栏的颜色 根据我的理解 导航栏顶部有一个默认背景 黑色 X

  • 从 fresco 获取 bitmapdrawable

    我正在尝试从 SimpleDraweeView 获取位图 我已经使用 uri 图像设置了 SimpleDraweeView final Uri uri new Uri Builder scheme UriUtil LOCAL RESOURC

  • 如何阻止 Docker 注册表？

    我想阻止对默认 docker io 注册表的访问 为了安全 IP 保护 我们需要阻止对公共 Docker 中心的推 拉访问 曾经有过many尝试将此作为配置选项 但所有 PR 都不断被拒绝 红帽已经实现了 block registry 和

  • java 图形的多线程

    我有一个java应用程序 可以传输原始数据并相应地绘制实时图 这是通过调用我编写的使用 Graphics 对象的类中的方法来处理的 我在重写的paintComponent方法中实现了算法 以根据最新数据生成所有绘图 我的类中有其他方法来更新

  • 同时在 dplyr 中对多列进行 Shapiro.test

    我正在尝试对数据集运行正态性检验 shapiro wilk 并且我希望同时获得所有列的统计数据和 p 值 我已阅读 SO 上的所有其他页面 R 按组进行的夏皮罗测试不会产生 p 值和损坏的数据框警告 https stackoverflow

  • 除了第一个之外，所有意图都收到了错误的附加内容

    我有一个小应用程序 可用于设置未来事件的提醒 该应用程序使用 AlarmManager 来设置提醒用户的时间 当闹钟响起时 BroadcastReceiver 会对此进行注册 然后启动一项服务 通过 Toast 和状态栏中的通知来通知用户

  • 控制进程停止后 Android Activity 重新启动

    我的应用程序正在运行 Android Gingerbread 2 3 7 自定义版本的特殊设备上运行 在某些情况下 系统将终止我的应用程序 我认为设备制造商考虑到了这些紧急情况 应立即关闭所有第三方应用程序 以便设备可以执行其主要任务 我可

  • 使用dispatch_sync作为互斥锁

    这是我需要做的 我希望dispatch sync是使用GCD实现这一点的最佳方法 我有一段关键部分代码放置在 Appdelegate 的 applicationDidBecomeActive 回调中 我将该方法包装在dispatch syn

  • 将scala生成的数据写入文本文件

    我希望有人可以提供帮助 我是 scala 新手 并且在将输出写入文本文件时遇到一些问题 我有一个数据表 并且编写了一些代码来一次读取一行 执行我想要它执行的操作 现在我需要它将该行写入文本文件 例如 我有下表的数据类型 名称 日期 goX

  • 为什么 Scala 在第一种情况下警告类型擦除而不是第二种情况？

    我有两个函数 这些函数自原始以来没有被编辑过 下面的一些答案是对返回 序列的原始函数的响应 def foo1 A ls Iterable A Iterator A for List a b lt ls sliding 2 yield a d

  • 将“输入”传递给 Theano 中的函数的目的/含义是什么？

    我希望示例会让这一点更清楚 这是一个 Logistic 回归对象 Theano 张量库作为 T 导入 def init self input n in n out Other code self p y given x T nnet sof

  • 如何在构造微积分中提取Sigma的第二个元素？

    我尝试这样做 A gt B A gt gt t r gt x a gt B x gt r gt r gt t B t A x A gt y B x gt x x A gt y B x gt y 请注意 由于该函数返回的值取决于 sigma

热门标签