如何解决我们如何将 Haskell 元组与 Agda 数据类型匹配?
我想在 Agda 中使用 Haskell 代码,例如,类似于返回整数和字符串对列表的函数。
我看到了这个文档: https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-function-interface.html
但我不知道如何将 Haskell 元组映射到 Agda 类型,因为例如在像
这样的映射中{-# COMPILE GHC APair = data ?????? #-}
我不知道如何填充 ????-s,因为我没有元组数据类型的定义。
但是,内置配对中也没有列出配对。
我应该如何进行?
解决方法
标准库在 Foreign.Haskell.Pair
(https://agda.github.io/agda-stdlib/Foreign.Haskell.Pair.html) 中执行此操作。相关代码是
record Pair (A : Set a) (B : Set b) : Set (a ⊔ b) where
constructor _,_
field fst : A
snd : B
open Pair public
{-# FOREIGN GHC type AgdaPair l1 l2 a b = (a,b) #-}
{-# COMPILE GHC Pair = data MAlonzo.Code.Foreign.Haskell.Pair.AgdaPair ((,)) #-}
在解释 Agda 类型中的 Universe 级别时需要稍加改动,这些级别未出现在 Haskell 对中。如果您不需要它,这应该就足够了:
data Pair (A B : Set) : Set where
_,_ : A → B → Pair A B
{-# COMPILE GHC Pair = data (,) ((,)) #-}
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。