例如,我想在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类型的宇宙水平,这些水平不会出现在Haskell对中。如果您不需要它,那么就足够了:
data Pair (A B : Set) : Set where
_,_ : A → B → Pair A B
{-# COMPILE GHC Pair = data (,) ((,)) #-}
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句