I am trying to create a type list that holds different transformers
type Transformers = [RWST, StateT]
Is there a way to define this list without a type wrapper?
No more than you could write [1, "two"] at the value level. Lists are homogeneous.
What’s the context? Perhaps type Transformers = (RWST, StateT) or a type-level HList would work for your use case?
I need to test many combinations of types for my parser printer library.
Described in Type Combinations for Tests
I would like to have lists of transformer, read, write, state, monad, and text types then
- apply a type function that gives all the combinations of these list
- apply a type function to each of the combinations to produce the type to apply to the tests
- use a class that folds over the type list and constructs the tests
I don’t understand how you can hope to uniformly (i.e., as a fold would) combine differently-kinded types. Can you try pseudocoding what you want to do in value-level Haskell, as if you were working with function values with different arities instead of type constructors with different kinds? That might clarify things for you and/or me.
Here is my incomplete foolhardy attempt so far
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
import Biparse.BiparserSpec qualified
main :: IO ()
main = hspec do
describe "forward" do
Biparse.BiparserSpec.specForward @(Fwd (StateErrorT (Position UnixLC (), String) (Either ((Position UnixLC (), String), String))))
-- Biparse.BiparserSpec.specForward @(Fwd (StateT (Position UnixLC (), String) IO))
-- Biparse.BiparserSpec.specForward @(Fwd (StateT (Position UnixLC (), String) IO))
-- Biparse.BiparserSpec.specForward @(Fwd (FileT String IO))
-- Biparse.BiparserSpec.specForward @(Fwd (FileT String (UpdateState (StateT (Position UnixLC FilePath) IO))))
-- Biparse.BiparserSpec.specForward @(Fwd (StateErrorT (Position UnixLC (), Text) (Either ((Position UnixLC (), Text), String))))
-- Biparse.BiparserSpec.specForward @(Fwd (StateT (Position UnixLC (), Text) IO))
-- Biparse.BiparserSpec.specForward @(Fwd (StateT (Position UnixLC (), Text) IO))
-- Biparse.BiparserSpec.specForward @(Fwd (FileT Text IO))
-- Biparse.BiparserSpec.specForward @(Fwd (FileT Text (UpdateState (StateT (Position UnixLC FilePath) IO))))
--describe "backward" do
-- Biparse.BiparserSpec.specBackward @(Bwd (WriterT String (Either String)))
-- Biparse.BiparserSpec.specBackward @(Bwd (WriterT String IO))
-- Biparse.BiparserSpec.specBackward @(Bwd (FileT String IO))
-- Biparse.BiparserSpec.specBackward @(Bwd (FileT String (StateT () IO)))
-- Biparse.BiparserSpec.specBackward @(Bwd (WriterT Text (Either String)))
-- Biparse.BiparserSpec.specBackward @(Bwd (WriterT Text IO))
-- Biparse.BiparserSpec.specBackward @(Bwd (FileT Text IO))
-- Biparse.BiparserSpec.specBackward @(Bwd (FileT Text (StateT () IO)))
type ForwardProfunctor :: transformer -> * {- read -} -> * {- write -} -> state -> monad -> * {- text -} -> * -> * -> *
newtype ForwardProfunctor transformer read write state monad text u a = ForwardProfunctor
( Fwd
( MakeTransMonad
transformer
read
write
(MakeState transformer state text)
( MakeMonad
transformer
read
write
(MakeState transformer state text)
text
(MakeSubMonad transformer read write (MakeState transformer state text) monad)
)
text
)
u
a
)
type MakeTransMonad :: transformer -> * -> * -> * -> (* -> *) -> * -> (* -> *)
type family MakeTransMonad transformer read write state monad text where
MakeTransMonad FileT _ _ _ m text = FileT text m
MakeTransMonad rwsT r w s m _ = rwsT r w s m
MakeTransMonad stateT _ _ s m _ = stateT s m
type MakeState :: transformer -> state -> * {- text -} -> *
type family MakeState transformer state text where
MakeState FileT s _ = s
MakeState _ s t = (s, t)
type MakeMonad :: transformer -> * {- read -} -> * {- write -} -> * {- state -} -> * {- text -} -> monad -> (* -> *)
type family MakeMonad transformer read write state text monad where
MakeMonad FileT _ _ _ _ IO = IO
MakeMonad FileT r w s _ rwsT = UpdateState (rwsT r w s IO)
MakeMonad FileT _ _ s _ stateT = UpdateState (stateT s IO)
MakeMonad _ _ _ _ _ m = m
--MakeMonad rwsT r w s _ m = rwsT r w s m
--MakeMonad stateT _ _ s _ m = stateT s m
type MakeSubMonad :: transformer -> * {- read -} -> * {- write -} -> * {- state -} -> monad -> (* -> *)
type family MakeSubMonad transformer monad read write state where
MakeSubMonad FileT _ _ _ IO = IO
MakeSubMonad FileT r w s m = MakeTransMonad m r w s IO ()
MakeSubMonad _ _ _ s Either = Either s
MakeSubMonad _ _ _ _ IO = IO
data Read
data Write
a :: ForwardProfunctor StateErrorT Read Write (Position UnixLC ()) Either Text () ()
a = ForwardProfunctor _
a' :: ForwardProfunctor StateErrorT Read Write (Position UnixLC ()) IO Text () ()
a' = ForwardProfunctor _
b :: ForwardProfunctor RWST Read Write (Position UnixLC ()) Either Text () ()
b = ForwardProfunctor _
b' :: ForwardProfunctor RWST Read Write (Position UnixLC ()) IO Text () ()
b' = ForwardProfunctor _
c :: ForwardProfunctor FileT Read Write (Position UnixLC ()) IO Text () ()
c = ForwardProfunctor _
d :: ForwardProfunctor FileT Read Write (Position UnixLC ()) StateT Text () ()
d = ForwardProfunctor _
e :: ForwardProfunctor FileT Read Write (Position UnixLC ()) RWST Text () ()
e = ForwardProfunctor _
type Transformers :: [*]
type Transformers = '[Poly RWST, Poly StateT]
type Reads :: [*]
type Reads = '[ () ]
type Writes :: [*]
type Writes = '[ () ]
type States :: [*]
type States = '[ Position UnixLC (), IndexPosition () ]
type Monads :: [*]
type Monads = '[Poly IO, Poly Either]
type Texts :: [*]
type Texts = '[String, Text]
type Poly :: k -> *
data Poly k
type Pairs :: [k] -> [l] -> [(k,l)] -> [(k,l)]
type family Pairs xs ys zs
type Associate :: k -> [l] -> [(k,l)] -> [(k,l)]
type family Associate x ys zs
That’s not terribly helpful, as it neither works nor communicates what it is you’re trying to do.
Again: if you had value-level functions of different arities instead of type constructors of different kinds, what Haskell code would you write to combine them in the desired way?
Thanks for the honest reply. I’ll try condensing this down a bit and post what I come up with.
Really gotta emphasize here that a condensing-down is not what I’m asking for.
Consider this:
data T = Str | Txt | Mbe T | Eth T T
f0s :: [T]
f0s = [Str, Txt]
f1s :: [T -> T]
f1s = [Mbe]
f2s :: [T -> T -> T]
f2s = [Eth]
allCombinations :: [T]
allCombinations =
f0s ++
(f1s <*> f0s) ++
(f2s <*> f0s <*> f0s)
This is one way of combining a bunch of functions of different arities. It may or may not correspond to what you’re looking for—for example, it does not recurse into itself to generate the arguments to the f2s. This is just one way of combining things of different arities.
Can you write a version of this code that contains analogs of the types and transformers you care about that does correspond to what you’re looking for? If you make data T an instance of Show, can you print the resulting list and check that it enumerates all the types that you care about? If you can do that, I can help you lift it to the type level.
1 Like
No, but what I think you mean is something like
type Transformers = [RWST Int String Bool, StateT Char]
which you can do if you turn on DataKinds. However, that still probably doesn’t allow you to do what you want, because you want to produce some value-level data from this type level data. In order to do that you’ll need a singleton, something like
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE ScopedTypeVariables #-}
class Runnable t where
run :: IO String
data TypeableList l where
SNil :: TypeableList '[]
SCons :: (Runnable a, KnownTypeableList l) => TypeableList (a ': l)
class KnownTypeableList a where
knownTypeableList :: TypeableList a
instance KnownTypeableList '[] where
knownTypeableList = SNil
instance (Runnable a, KnownTypeableList l) => KnownTypeableList (a ': l) where
knownTypeableList = SCons
example :: forall l. KnownTypeableList l => IO [String]
example = case knownTypeableList @l of
SNil -> pure []
SCons @a @l' -> do
a1 <- run @a
l1 <- example @l'
pure (a1 : l1)
Replace the Runnable constraint with whatever constraint it is that the types you pass to specForward must satisfy.
Thanks this is very helpful. Makes me wish we could pass type functions so I do not have to define TypeableList for the differing constraints of each suite of tests.
You don’t need type functions for this, just something like a pi.
class Pi f a b where
applyPi :: f -> Proxy a -> b
-- This requires GHC 9.10 (-XRequiredTypeArguments) but without it
-- you can do all the same things, just with more Proxy noise
infixl 9 @
(@) :: forall f. f -> forall a -> forall b. Pi f a b => b
f @ a = f `applyPi` Proxy @a
newtype Traverse f = Traverse f
instance Applicative m => Pi (Traverse f) '[] (m [b]) where
applyPi _ _ = pure []
instance (Applicative m, Pi f h (m b), Pi (Traverse f) t (m [b])) => Pi (Traverse f) (h ': t) (m [b]) where
applyPi (Traverse f) _ = (:) <$> f @ h <*> Traverse f @ t
-- Just these bits need to be redefined for additional functions with different constraints:
data MyTestFunction = MyTestFunction -- any non-type-dependent arguments here
instance ({-- constraints here --}) => Pi MyTestFunction t (IO String) where
applyPi _ _ = undefined -- implementation here
-- End of bits
type ListOfTypes = '[RWST Int String Bool, StateT Char]
example :: IO [String]
example = Traverse MyTestFunction @ ListOfTypes
I think this will work
data TypeableList c l where
SNil :: TypeableList '[]
SCons :: (c a, KnownTypeableList l) => TypeableList (a ': l)
I was looking for this but I’m only on 9.2 so Proxy it is.