[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

OK, here's my attempt to patch things.  The goal is to provide FFI 
bindings for level-polymorphic datatypes (and if we happen to do some 
other dependencies while we're at it, then so much the better).

One slight wrinkle is that it's not obvious what the success criteria 
are.  I'm guessing the goal is that any program which successfully 
compiles shouldn't produce any errors due to coercion, which can 
probably be formalized using contract types, and blaming, together with 
a result that says that if Agda is blamed, then there is a Haskell-free 
program with the same runtime error, and dually if Haskell is blamed.

Brain-dump for a modification to the compiler follows.  After that, an 
implementation, which should be straightforward, ho ho ho.

The core of the existing translation is:

    K[[ Set A ]] = *
    K[[ x As ]] = undef
    K[[ fn (x : A) B ]] = undef
    K[[ Pi (x : A) B ]] = K[[ A ]] ->  K[[ B ]]
    K[[ k As ]] = undef

    T[[ Set A ]] = undef
    T[[ x As ]] = x T[[ As ]]
    T[[ fn (x : A) B ]] = undef
    T[[ Pi (x : A) B ]] =
      if K[[ A ]] is defined
      then forall x . Unit ->  T[[ B ]]
      else if x in fv B
      then undef
      else T[[ A ]] ->  T[[ B ]]
    T[[ k As ]] =
      if COMPILED_TYPE k T
      then T T[[ As ]]
      else undef

    E[[ Set A ]] = unit
    E[[ x As ]] = x E[[ As ]]
    E[[ fn (x : A) B ]] = fn x . E[[ B ]]
    E[[ Pi (x : A) B ]] = unit
    E[[ k As ]] =
      if COMPILED k E
      then E E[[ As ]]
      else runtime-error

The change to get many uses of level-polymorphism to go through is:

    K[[ k As ]] =
      if COMPILED_TYPE k
      then *
      else undef

    T[[ Set A ]] = Unit
    T[[ Pi (x : A) B ]] =
      if x in fv B
      then forall x . T[[ A ]] -> T[[ B ]]  -- Note: T[[A]] not Unit
      else T[[ A ]] -> T[[ B ]]

Now, this isn't exactly backwards compatible, as there are some 
translations which have changed, for example:

   T[[ (Set -> Set) -> Set -> Set ]]
     was Unit -> Unit -> Unit
     now (Unit -> Unit) -> Unit-> Unit

However, this is actually a more accurate type, and indeed at runtime 
expressions of this type will be fed functions, not unit values.

For example, on dependently-typed IO (assuming Level is bound to Int) we 
get:

   postulate
     IO : {a : Level} -> (b : Set a) -> (Set a)
     return : {a : Level} -> {b : Set a} -> b -> (IO b)
     _>>=_ : {a b : Level} -> {c : Set a} -> {d : Set b} ->
       (IO c) -> (c -> (IO d)) -> (IO d)

   {-# COMPILED_TYPE IO AgdaIO #-}
   {-# COMPILED return (\_ _ -> return) #-}
   {-# COMPILED _>>=_ (\_ _ _ _ -> (>>=)) #-}

where type AgdaIO a b = IO b.  This typechecks because:

   AgdaIO
      : * -> * -> *
     = K [[ {a : Level} -> (b : Set a) -> (Set a) ]]

   (\_ _ -> return)
     : forall a -> Int -> forall b -> Unit -> b -> (AgdaIO a b)
     = T [[ {a : Level} -> {b : Set a} -> b -> (IO {a} b) ]]

   (\_ _ _ _ -> (>>=))
     : forall a -> Int -> forall b -> Int ->
         forall c -> Unit -> forall d -> Unit ->
           (AgdaIO a c) -> (c -> (AgdaIO b d)) -> (AgdaIO b d)
     = T [[ {a b : Level} -> {c : Set a} -> {d : Set b} ->
              (IO {a} c) -> (c -> (IO {b} d)) -> (IO {b} d) ]]

Boy, that was a bit of a slog.

A.

On 09/24/2010 11:45 AM, Jeffrey, Alan S A (Alan) wrote:
> On 09/23/2010 11:43 PM, Nils Anders Danielsson wrote:
>> On 2010-09-20 14:34, Alan Jeffrey wrote:
>>> The source of these errors is HaskellTypes.hs -- it looks like there'd
>>> be an easy fix for universe-monomorphic bindings, which is to add a
>>> cluase to haskellType, something like:
>>>
>>> Lit (LitLevel _ _) ->   "()"
>>
>> This seems wrong, because there is nothing which stops an Agda program
>> from pattern matching on a level. I hope that we will switch to
>> parametric universe-polymorphism soon, but this has not happened yet.
>
> OK, deep breath, my thoughts by me...
>
> There's (essentially) three translations from Agda to Haskell, one from
> kinds, one from well-kinded types, and one from well-typed expressions,
> e.g.:
>
>     K[[ Set M ]] = *
>     K[[ x A1 ... An ]] = undef
>     K[[ fn (x : A) B ]] = undef
>     K[[ Pi (x : A) B ]] = K[[ A ]] ->  K[[ B ]]
>
>     T[[ Set M ]] = undef
>     T[[ x A1 ... An ]] = x T[[ A1 ]] ... T[[ An ]]
>     T[[ fn (x : A) B ]] = undef
>     T[[ Pi (x : A) B ]] =
>       if K[[ A ]] is defined
>       then forall x . () ->  T[[ B ]]
>       else if x in fn B
>       then undef
>       else T[[ A ]] ->  T[[ B ]]
>
>     E[[ Set M ]] = ()
>     E[[ x A1 ... An ]] = x E[[ A1 ]] ... E[[ An ]]
>     E[[ fn (x : A) B ]] = fn x . E[[ B ]]
>     E[[ Pi (x : A) B ]] = ()
>
> The proposed treatment of levels is:
>
>     K[[ Level ]] = *
>     T[[ Level ]] = Int
>     E[[ Level ]] = ()
>
>     K[[ level n ]] = undef
>     T[[ level n ]] = ()
>     E[[ level n ]] = n
>
> Now, you're right there is a problem, because we can have functions that
> treat levels just as regular datatypes, e.g.
>
>     data Foo : Level ->  Set where
>       foo : (a : Level) ->  (Foo a)
>
>     x : Foo zero
>     x = foo zero
>
> breaks because the translation ends up with:
>
>     foo : forall a . () ->  (Foo a)
>     x : Foo ()
>     x = foo 0
>
> The translation should actually be:
>
>     foo : forall a . Int ->  Foo a
>
> I'll have to think about how to fix this, a first shot is:
>
>     T[[ Pi (x : A) B ]] =
>       if K[[ A ]] is defined
>       then if T[[ A ]] is defined
>         then forall x . T[[ A ]] ->  T[[ B ]]
>         else forall x . () ->  T[[ B ]]
>       else ... as before ...
>
> but this doesn't work, e.g. when A is itself a variable.
>
> A.