级联函数列表的类型是什么？

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 

请注意，这不考虑中间函数的类型，因此它可能不是您要查找的内容。

---

我刚刚意识到这与[c - > d，b - > c，a - > b]更接近。让它更接近你的意图是一个容易的改变;我可以编辑它，但我认为你明白了。

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