[Agda] Re: Agda FFI bindings
Alan Jeffrey
ajeffrey at bell-labs.com
Thu Sep 30 22:05:36 CEST 2010
Here's my implementation of the translation defined below. It patches
the compiler, changing the definition of "Haskell type" and "Haskell
kind", and the standard library to give Level, Data.Maybe, etc. FFI
bindings.
This is still in a bit of a draft state, especially because I'm not sure
what makes for a good test suite.
A.
On 09/28/2010 04:40 PM, Jeffrey, Alan S A (Alan) wrote:
> 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.
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: UniversePolymorphismFFI.patch
Type: text/x-patch
Size: 2821 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100930/d01f6f30/UniversePolymorphismFFI.bin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: StdLibFFI.patch
Type: text/x-patch
Size: 2358 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100930/d01f6f30/StdLibFFI.bin
More information about the Agda
mailing list