Ryan Newton
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.