What will be the type of cascading function list?

In Haskell syntax, we can have a (abstract) type type [a -> b] , which is a list of functions from a to b. The specific type of this would be [Int -> Int] , for example map (*) [1..10] . Is it possible to have a list of cascading functions in a type like [a -> b, b -> c, c -> d, ...] ? The individual list items are all different (I think), so I don’t think that this is possible. But is this possible with dependent types? What would his type signature be (preferably in pseudo-Haskell syntax)?

+1
source share
3 answers

You cannot do this with a simple list, but you can create your own list type, as shown below:

 {-# LANGUAGE GADTs #-} data CascadingList io where Id :: CascadingList ii Cascade :: (b -> o) -> CascadingList ib -> CascadingList io 

Then you can do these CascadingList as follows:

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

You can collapse lists:

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

Then you will have

 collapse addOnePositive 0 == True 

Please note that this does not take into account the types of intermediate functions, so this may not be what you are looking for.


I just realized that this is closer to something like [c β†’ d, b β†’ c, a β†’ b]. This is an easy change to bring it closer to your intentions; I could edit it, but I think you get the point.

+6
source

Using DataKinds , you can open internal collection types that can facilitate the use of components:

 {-# 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 (fa) -- 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) = fa ': 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 -> mb) -> 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 =<< fa 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 
+5
source

A slight improvement in the response of scrambledeggs, referring to some comments:

 {-# LANGUAGE GADTs #-} import Data.Typeable data CascadingList io where Id :: CascadingList ii Cascade :: Typeable b => (b -> o) -> CascadingList ib -> CascadingList io 

Now that you have a match template on Cascade , you can at least try to guess what type of b is using the eqT button and cast functions from Data.Typeable , and if you guessed it, you can actually use the internal functions. Soft flaw - this only works for types with an instance of Typeable (which, at least, can get GHC).

+3
source

Source: https://habr.com/ru/post/1205518/


All Articles