[Agda] Re: Agda FFI bindings

[Alan Jeffrey]

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[[ lambda (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[[ lambda (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[[ lambda (x : A) B ]] = lambda 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.