【问题标题】:What would the type of a list of cascading functions be?级联函数列表的类型是什么?
【发布时间】:2014-12-22 23:11:57
【问题描述】:

在 Haskell 语法中,我们可以有一个像 [a -> b] 这样的(抽象)类型,它是函数 a 到 b 的列表。具体类型是[Int -> Int],例如map (*) [1..10]。是否可以有一个类似[a -> b, b -> c, c -> d, ...] 的类型的级联函数列表?列表中的各个元素都是不同的(我认为),所以我认为这是不可能的。但是依赖类型有可能吗?它的类型签名是什么(最好是伪 Haskell 语法)?

【问题讨论】:

  • 你不能用 Haskell 中的普通列表来做到这一点,但这是可能的。查看 HList 库中的异构列表。请注意,该库使用了很多扩展来获得这种动态行为。
  • 这是 jamshidh 链接的问题(子集)的副本。然而,这个问题更直接地说明了这个问题。

标签: haskell types type-systems dependent-type


【解决方案1】:

你不能用一个普通的列表来做到这一点,但你可以构造你自己的类似列表的类型,如下所示:

{-# LANGUAGE GADTs #-}

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

那么你可以将这些CascadingLists 制作成如下:

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

注意这里没有考虑中间函数的类型,所以可能不是你要找的。​​p>


我刚刚意识到这更接近于 [c -> d, b -> c, a -> b]。让它更接近你的意图是一个简单的改变;我可以编辑它,但我想你明白了。

【讨论】:

  • 正如我在answer to the previous question 中指出的那样,后续问题(和观察)是:这样的集合在函数组合方面为您提供了什么? (同样的构造用不同的Category 可能是另外一回事……)
  • 我可以看到的一个潜在优势是您可以从这种结构中提取组合函数,但简单的函数组合并非如此。一个人为的例子:(+1) . (-1) == (-1) . (+1),但是[(+1),(-1)] /= [(-1),(+1)](显然是滥用符号)。
  • 是的,我也注意到了。但是你不能用它们做很多事情。除此之外,您无法从 GADT 之外预测它们的类型。
【解决方案2】:

使用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

【讨论】:

  • 我认为Chain 也可以实现为(封闭的)类型族,因为类型参数cs 准确地规定了将使用哪些构造函数。
  • Christian Conkle:是的,我做到了here for OneOf。我现在正在玩弄它。
  • Christian Conkle:我暂时放弃了封闭类型族,因为当我尝试做任何有趣的事情时,我不断遇到单射类型错误。
【解决方案3】:

对 scrambledeggs 的回答进行了小幅改进,解决了一些 cmets:

{-# 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 进行模式匹配时,您至少可以尝试使用the eqT and cast functions from Data.Typeable 猜测b 是哪个类型,如果您猜对了,您实际上可以使用内部函数。轻微的缺点是它仅适用于具有 Typeable 实例的类型(至少 GHC 可以派生)。

【讨论】:

    猜你喜欢
    • 1970-01-01
    • 2021-09-04
    • 1970-01-01
    • 1970-01-01
    • 2016-10-06
    • 1970-01-01
    • 1970-01-01
    • 2020-05-18
    • 1970-01-01
    相关资源
    最近更新 更多