Каким будет тип списка каскадных функций?

Question

В синтаксисе Haskell мы можем иметь (абстрактный) тип, такой как [a -> b], который представляет собой список функций от a до b. Конкретным типом этого будет [Int -> Int], например map (*) [1..10]. Возможно ли иметь список каскадных функций в типе типа [a -> b, b -> c, c -> d, ...]? Отдельные элементы списка все разные (я думаю), поэтому я не думаю, что это возможно. Но возможно ли это с зависимыми типами? Какова была бы его подпись типа (предпочтительно в синтаксисе псевдо-Хаскелла)?

Answer 1

Вы не можете сделать это с помощью простого списка, но вы можете построить свой собственный список, как тип следующим образом:

{-# LANGUAGE GADTs #-} 

data CascadingList i o where 
    Id :: CascadingList i i 
    Cascade :: (b -> o) -> CascadingList i b -> CascadingList i o 

Тогда вы могли бы сделать эти CascadingList S следующим образом:

addOnePositive :: CascadingList Int Bool 
addOnePositive = Cascade (>0) $ Cascade (+1) $ Id 

вы могли бы 'коллапс' списки:

collapse :: CascadingList a b -> a -> b 
collapse Id = id 
collapse (Cascade f c) = f . collapse c 

Тогда вы бы

collapse addOnePositive 0 == True 

Обратите внимание, что это не учитывает типы промежуточных функций, поэтому, возможно, это не то, что вы ищете.

---

Я просто понял, что это ближе к чему-то вроде [с -> d, Ь -> с, а -> Ь]. Это легкое изменение, чтобы приблизить его к вашим намерениям; Я мог бы его отредактировать, но, думаю, вы поняли.

Answer 2

небольшое улучшение на ответ scrambledeggs', обращаясь к некоторым из комментариев:

{-# LANGUAGE GADTs #-} 

import Data.Typeable 

data CascadingList i o where 
    Id :: CascadingList i i 
    Cascade :: Typeable b => (b -> o) -> CascadingList i b -> CascadingList i o 

Теперь, когда вы подходите картины на Cascade, вы можете по крайней мере попытаться угадать, какой тип b является использование the eqT and cast functions from Data.Typeable, и если вы догадываетесь, что вы действительно можете использовать внутренние функции. Мягкий минус - он работает только для типов, имеющих экземпляр Typeable (который, по крайней мере, может получить GHC).

Answer 3

Использования DataKinds, вы можете выставить внутренние типы коллекции, которые могут сделать с помощью составных частей проще:

{-# LANGUAGE PolyKinds #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE GADTs #-} 
module Cascade where 
import Control.Monad ((>=>), liftM) 
import Control.Category ((>>>)) 

data Cascade (cs :: [*]) where 
    End :: Cascade '[a] 
    (:>>>) :: (a -> b) -> Cascade (b ': cs) -> Cascade (a ': b ': cs) 
infixr 5 :>>> 

-- a small example 
fs :: Cascade '[ String, Int, Float ] 
fs = read :>>> fromIntegral :>>> End 

-- alternate using functions from one chain then the other 
zigzag :: Cascade as -> Cascade as -> Cascade as 
zigzag End End = End 
zigzag (f :>>> fs) (_ :>>> gs) = f :>>> zigzag gs fs 

-- compose a chain into a single function 
compose :: Cascade (a ': as) -> a -> Last (a ': as) 
compose End = id 
compose (f :>>> fs) = f >>> compose fs 

-- generalizing Either to a union of multiple types 
data OneOf (cs :: [*]) where 
    Here :: a -> OneOf (a ': as) 
    There :: OneOf as -> OneOf (a ': as) 

-- start the cascade at any of its entry points 
fromOneOf :: Cascade cs -> OneOf cs -> Last cs 
fromOneOf fs (Here a) = compose fs a 
fromOneOf (_ :>>> fs) (There o) = fromOneOf fs o 

-- generalizing (,) to a product of multiple types 
data AllOf (cs :: [*]) where 
    None :: AllOf '[] 
    (:&) :: a -> AllOf as -> AllOf (a ': as) 
infixr 5 :& 

-- end the cascade at all of its exit points 
toAllOf :: Cascade (a ': as) -> a -> AllOf (a ': as) 
toAllOf End a  = a :& None 
toAllOf (f :>>> fs) a = a :& toAllOf fs (f a) 

-- start anywhere, and end everywhere after that 
fromOneOfToAllOf :: Cascade cs -> OneOf cs -> OneOf (Map AllOf (Tails cs)) 
fromOneOfToAllOf fs (Here a) = Here $ toAllOf fs a 
fromOneOfToAllOf (_ :>>> fs) (There o) = There $ fromOneOfToAllOf fs o 

-- type level list functions 
type family Map (f :: a -> b) (as :: [a]) where 
    Map f '[] = '[] 
    Map f (a ': as) = f a ': Map f as 

type family Last (as :: [*]) where 
    Last '[a] = a 
    Last (a ': as) = Last as 

type family Tails (as :: [a]) where 
    Tails '[] = '[ '[] ] 
    Tails (a ': as) = (a ': as) ': Tails as 

-- and you can do Monads too! 
data CascadeM (m :: * -> *) (cs :: [*]) where 
    EndM :: CascadeM m '[a] 
    (:>=>) :: (a -> m b) -> CascadeM m (b ': cs) -> CascadeM m (a ': b ': cs) 
infixr 5 :>=> 

composeM :: Monad m => CascadeM m (a ': as) -> a -> m (Last (a ': as)) 
composeM EndM = return 
composeM (f :>=> fs) = f >=> composeM fs 

fromOneOfM :: Monad m => CascadeM m cs -> OneOf cs -> m (Last cs) 
fromOneOfM fs (Here a) = composeM fs a 
fromOneOfM (_ :>=> fs) (There o) = fromOneOfM fs o 

-- end the cascade at all of its exit points 
toAllOfM :: Monad m => CascadeM m (a ': as) -> a -> m (AllOf (a ': as)) 
toAllOfM EndM a  = return $ a :& None 
toAllOfM (f :>=> fs) a = do 
    as <- toAllOfM fs =<< f a 
    return $ a :& as 

-- start anywhere, and end everywhere after that 
fromOneOfToAllOfM :: Monad m => CascadeM m cs -> OneOf cs -> m (OneOf (Map AllOf (Tails cs))) 
fromOneOfToAllOfM fs (Here a) = Here `liftM` toAllOfM fs a 
fromOneOfToAllOfM (_ :>=> fs) (There o) = There `liftM` fromOneOfToAllOfM fs o