[Agda] Interfacing with Haskell

[Nils Anders Danielsson]

On 2009-11-22 13:17, Ivan Tomac wrote:
> Is there a way to map or import a type like Int from Haskell to Agda?

module Int where

open import IO
open import Data.Function
open import Data.String

postulate
  Int  : Set
  #0   : Int
  gcd  : Int → Int → Int
  show : Int → String

{-# COMPILED_TYPE Int Int #-}
{-# COMPILED #0   (0 :: Int) #-}
{-# COMPILED gcd  (gcd :: Int -> Int -> Int) #-}
{-# COMPILED show (show :: Int -> String) #-}

main = run $
  putStrLn $ show $ gcd #0 #0

-- $ ./Int
-- Int: GHC.Base.gcdInt: gcd 0 0 is undefined

> Both seem awkward. Is there a better way to do this?

f : {A : Set} → A → A × A
f a = ?

g : {A : Set} → A → A
g a with f a
... | (a' , _) = a'

--
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.