[Haskell-cafe] FunPtr to C function with #arguments determined atruntime?

[Ertugrul Söylemez]

Ryan Newton <rrnewton at gmail.com> wrote:

> My problem is that I can't create a type representing what I want at
> the Haskell type-check time, and I need such a type for either
> casting or a foreign import.  For example, let's say the function
> takes a number of Int arguments between 1 and 1000.  If I find out at
> runtime that I need a function with 613 Int arguments, I would need
> to create the type (Int -> Int ... -> IO ()) to cast to.  I suppose
> there may be some way to create such a dependent type with
> Typeable/Data.Dynamic, since it's monomorphic. Or in theory you could
> dynamically generate new Haskell code to create the type
> (System.Eval.Haskell)...

Simpler.  This is our goal:

    main :: IO ()
    main = withFunction (push 3 $ push 4 $ done)

The withFunction function constructs a function at run-time, say, by
reading a file, yet this is completely type-safe, statically checked
code and also looks quite nice.

First make a clear separation between the producer and consumer of a
type.  The producer constructs the type, the consumer uses it.  Then you
can use either existentials or higher-rank types.  Let's say the user
enters a number, and we want to treat it as Integer if possible,
otherwise as Double.  This is the traditional approach:

    withNum :: String -> b -> (Integer -> b) -> (Double -> b) -> b
    withNum str none ki kd
        | [(x, _)] <- reads str = ki x
        | [(x, _)] <- reads str = kd x
        | otherwise = none

Here is an improved variant:

    withNum :: String -> b -> (forall a. (Num a) => a -> b) -> b
    withNum str none k
        | [(x, _)] <- reads str = k (x :: Integer)
        | [(x, _)] <- reads str = k (x :: Double)
        | otherwise = none

This is almost the same function, but with an important difference.  For
both cases the same continuation is called, because withNum accepts only
functions that can promise to work "for all" numeric types.  In other
words, the function must be polymorphic enough.  What really happens
here is that I determine the type at run-time depending on the string.
That's how lightweight dependent types work.  Meet withFunction from the
teaser.  It reveals only its type signature for now:

    withFunction ::
        (forall a. (Push a) => a -> IO b)
        -> IO b

The withFunction function lifts something from value level and
constructs a function of the correct type from it.  Whatever the
continuation receives is a function of the proper type.  However, you
can't just call the function yet, because withFunction's argument
promises that it works for every type 'a'.  So it can't just pass it an
Int.  That's where the Push class comes in.  Here is a very simple,
non-fancy Int-only way to define it:

    class Push a where
        push :: Int -> (forall b. (Push b) => b -> IO c) -> a -> IO c
        done :: a -> IO ()

    instance (Push a) => Push (Int -> a) where
        push x k f = k (f x)
        done _ = throwIO (userError "Messed up my arguments, sorry")

    instance Push (IO ()) where
        push _ _ _ = throwIO (userError "Messed up my arguments, sorry")
        done = id

Don't worry about the scary types.  They are actually pretty simple:
The push function, if possible, applies the given Int (first argument)
to the given function (third argument).  It passes the result to the
continuation (second argument), which again promises to work for every
Push.  For non-functions a run-time exception is raised (obviously you
can't do that at compile time, so this is the best we can get).  Here is
an example withFunction together with its application:

    withFunction k =
        let f :: Int -> Int -> IO ()
            f x y = print x >> print y
        in k f

    main :: IO ()
    main = withFunction (push 3 $ push 4 $ done)

Ain't that nice?

Of course the FunPtr is now implicit in whatever withFunction constructs
it from.  While you still need the foreign declaration you now get
type-safety for types determined at run-time.  If the constructed
function takes another Int argument, push is the way to apply it.

I hope this helps.


Greets,
Ertugrul

-- 
Not to be or to be and (not to be or to be and (not to be or to be and
(not to be or to be and ... that is the list monad.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130219/af8ab740/attachment.pgp>