How can we match Haskell tuples to an Agda datatype?

Question

I would like to use Haskell code in Agda, for example, something like a function that gives back a list of pairs of integers and strings.

I saw this documentation: https://agda.readthedocs.io/en/v2.6.1.1/language/foreign-function-interface.html

But I don't know how to map Haskell tuples to an Agda type, because for example in a mapping like

{-# COMPILE GHC APair = data ?????? #-}

I don't know how to fill the ????-s, as I don't have the definition of the tuple data type.

However, pairs are not listed at the builtin pairings either.

How should I proceed?

ulfnorell ulfnorell · Accepted Answer · 2021-01-30T13:25:35

The standard library does this in Foreign.Haskell.Pair (https://agda.github.io/agda-stdlib/Foreign.Haskell.Pair.html). The relevant code is

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 ((,)) #-}

There's a little bit of fiddling to account for the universe levels in the Agda type, which don't appear in the Haskell pairs. If you don't need that, this should suffice:

data Pair (A B : Set) : Set where
  _,_ : A → B → Pair A B

{-# COMPILE GHC Pair = data (,) ((,)) #-}

How can we match Haskell tuples to an Agda datatype?

1 Answers