如何解决Agda用于对JavaScript数组建模的数据类型
在Agda中,我试图编写一些具有作用于它们的函数的数据类型。这些将被编译为javascript,用于验证应用程序状态的逻辑。为了做到这一点,我需要一个可编译为javascript数组的数据类型。我需要做一些过滤以及获取数组的最大值。
在Agda方面,我想证明这种数据类型的一些属性(将编译为javascript数组)。在std-lib
中,可以使用Vec
为javascript数组建模吗?还有其他选择(例如Vec.Bounded
等)吗?
我最初尝试使用Data.List
,但是有一个证明涉及到获取最后一个元素,因此我选择切换到Data.Vec
,以便不必处理Data.Maybe
。
稍后我想filter
列出一些元素,发现Data.Vec.filter
具有签名:
filter : ∀ {n} → Vec A n → Vec≤ A n
过滤掉元素后,我需要将Vec≤
转换回Vec
。
我想知道是否应该不使用Vec≤
来处理Vec≤
和Vec
之间的转换。
在编译为javascript时,这些不同数据类型之间需要进行哪些取舍? List
,Vec
和Vec≤
是否实际上全部都编译为JavaScript数组?另外,从Vec≤
支持List
和Vec
的功能的角度来看,它们是其他集合的超集吗?
谢谢!
解决方法
真正的“伸出来,在这里”是词: Javascript。
您究竟打算如何将[...]转换为Javascript 代码 ...,以获得Javascript 数据类型 ... (一个数组)...“
... ...我不知道你要去哪里。或者,认为您正在使用它。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。