Опускание функций на встроенный язык

Question

Как я могу опустить функцию Haskell на встроенный язык в качестве типичного способа, насколько это возможно. В частности, давайте предположим, что у меня есть тип значения, как

data Type t where 
    Num :: Type Int 
    Bool :: Type Bool 

data Ty = TNum | TBool deriving Eq 

data Tagged t = Tagged (Type t) t deriving Typeable 
data Dynamic = forall t . Typeable t => Dynamic (Tagged t) deriving Typeable 

forget :: Typeable t => Tagged t -> Dynamic 
forget = Dynamic 

remember :: Typeable b => Dynamic -> Maybe b 
remember (Dynamic c) = cast c 

и я хочу, чтобы преобразовать функцию как (isSucc :: Int -> Int -> Bool) произведению его динамической формы и некоторой информации о типе, как это

data SplitFun = SF { dynamic :: [Dynamic] -> Dynamic 
        , inputTypes :: [Ty] 
        , outputType :: Ty 
        } 

, что для некоторые apply функции

(\(a:b:_) -> isSucc a b) == apply (makeDynamicFn isSucc) 

по модулю некоторых возможных исключений, которые могли бы возникнуть, если динамические типы фактически не совпадают. Или, более конкретно, я бы хотел найти makeDynamicFn :: FunType -> SplitFun. Очевидно, что это не правильный тип Haskell и там вряд ли будет способ вывести типы из самого isSucc, так что это может быть что-то еще, как

anInt . anInt . retBool $ isSucc :: SplitFun 

где anInt и retBool имеют printf -Style типы.

Возможно ли такое? Есть ли способ имитировать это?

Answer 1

Для реализации функции типа FunType -> SplitFun мы будем использовать машины класса стандартного типа для деконструирования типов функций.

Теперь реализация этой функции оказывается довольно сложной. Чтобы получить inputTypes и outputType из рекурсивного случая, вам необходимо применить свою функцию; но вы можете применять эту функцию только внутри поля dynamic, что не дает возможности заполнить другие поля. Вместо этого мы разделим задачу на две: одна функция даст нам информацию Ty, другая построит функцию [Dynamic] -> Dynamic.

data Proxy a = Proxy 

class Split r where 
    dynFun :: r -> [Dynamic] -> Dynamic 
    tyInfo :: Proxy r -> ([Ty], Ty) 

    split :: r -> SplitFun 
    split f = let (i, o) = tyInfo (Proxy :: Proxy r) 
       in SF (dynFun f) i o 

Теперь tyInfo фактически не нужна функция, мы используем Proxy только для передачи информации о типе без необходимости использовать undefined повсюду. Обратите внимание, что нам нужно ScopedTypeVariables, чтобы иметь возможность ссылаться на переменную типа r из декларации экземпляра. Также может быть полезно использование asTypeOf.

У нас есть два базовых случая: Bool и Int:

instance Split Int where 
    dynFun i _ = forget (Tagged Num i) 
    tyInfo _ = ([], TNum) 

instance Split Bool where 
    dynFun b _ = forget (Tagged Bool b) 
    tyInfo _ = ([], TBool) 

Там нет типов входных и поскольку у нас уже есть значение, мы не должны просить больше Dynamic значений и мы просто возвращаем Dynamic из это особое значение.

Далее, мы имеем два случая: рекурсивные Bool -> r и Int -> r

instance (Split r) => Split (Int -> r) where 
    dynFun f (d:ds) = case remember d :: Maybe (Tagged Int) of 
     Just (Tagged _ i) -> dynFun (f i) ds 
     Nothing   -> error "dynFun: wrong dynamic type" 
    dynFun f []  = error "dynFun: not enough arguments" 

    tyInfo _ = case tyInfo (Proxy :: Proxy r) of 
     (i, o) -> (TNum:i, o) 

instance (Split r) => Split (Bool -> r) where 
    dynFun f (d:ds) = case remember d :: Maybe (Tagged Bool) of 
     Just (Tagged _ b) -> dynFun (f b) ds 
     Nothing   -> error "dynFun: wrong dynamic type" 
    dynFun f []  = error "dynFun: not enough arguments" 

    tyInfo _ = case tyInfo (Proxy :: Proxy r) of 
     (i, o) -> (TBool:i, o) 

Эти две потребности FlexibleInstances. dynFun проверяет первый аргумент Dynamic, и если все в порядке, мы можем безопасно применить к нему функцию f и продолжить оттуда. Мы могли бы также сделать dynFun :: r -> [Dynamic] -> Maybe Dynamic, но это довольно тривиальное изменение.

---

Теперь происходит некоторое дублирование. Мы могли бы представить еще один класс, например:

class Concrete r where 
    getTy :: Proxy r -> Ty 
    getType :: Proxy r -> Type r 

А потом пишут:

instance (Typeable r, Concrete r) => Split r where 
    dynFun r _ = forget (Tagged (getType (Proxy :: Proxy r)) r) 
    tyInfo _ = ([], getTy (Proxy :: Proxy r)) 

instance (Typeable r, Concrete r, Split s) => Split (r -> s) where 
    dynFun f (d:ds) = case remember d :: Maybe (Tagged r) of 
     Just (Tagged _ v) -> dynFun (f v) ds 
     -- ... 

    tyInfo _ = case tyInfo (Proxy :: Proxy s) of 
     (i, o) -> (getTy (Proxy :: Proxy r):i, o) 

Но это нужно как OverlappingInstances и UndecidableInstances.