級聯函數列表的類型是什麼？

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