[Agda] Interfacing with Haskell

[Ivan Tomac]

Nils Anders Danielsson wrote:
> 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
>

Oh, right. Is there a way to map the whole range of Int-s to some type 
in Agda? So that in the compiled code (suc zero) gets replaced with 1 
for example.

>> 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'
>

I forgot to mention I tried that too. I couldn't figure out how to get 
that to work with more than one expression. Here's a better example:

data State (S A : Set) : Set where
    St : (S → S × A) → State S A

apply : ∀ {s a b} → State s (a → b) → State s a → State s b
apply {s} {a} {b} (St sf) (St sa) = St (g sf sa)
    where
    g : (s → s × (a → b)) → (s → s × a) → (s → s × b)
    g sf sa s0 = map id (proj₂ s1f) s2a
        where
        s1f = sf s0
        s2a = sa (proj₁ s1f)

applicative : ∀ {S} -> RawApplicative (State S)
applicative = record
  { pure = λ a → St (λ s → (s , a))
  ; _⊛_ = apply
  }


I'd like to be able to write apply more like this:

apply : ∀ {s a b} → State s (a → b) → State s a → State s b
apply {s} {a} {b} (St sf) (St sa) = St (g sf sa)
    where
    g : (s → s × (a → b)) → (s → s × a) → (s → s × b)
    g sf sa s0 = (s2 , f a)
        where
        (s1 , f) = sf s0
        (s2 , a) = sa s1

But that doesn't work due to missing type signatures for s1, s2, f and a 
and I can't figure out how to add the signatures.