What can be computed on left side of the fat arrow?
Hello, I was exploring haskell and got to the point where it seems that there are only a few people who could answer my question, many of whom are involved in the development of ghc. I hope you don't mind that I ask it here for I spend too much time in a barren waiting. Here is the question:
Suppose, you have a type like this
data HList :: [*] -> * where
Cons :: p -> HList a -> HList (p ': a)
End :: HList '[]
My intention is to define a record type by requiring any type that is generated by HList
to have its left
component (Cons a End
here a is left component) to be of kind Pair Symbol *
.
To do this I planned to use a type family that will compute whether a type is compliant to the requirement or not with this code:
type CSat = () :: Constraint
type CNSat = Int ~ Bool
type family RecurseAndCheck a (b :: HList t) where
-- if left component is of kind a then continur
RecurseAndCheck a (Cons (b :: a) r) = RecurseAndCheck a r
-- if it's end, no error occured
RecurseAndCheck a End = CSat
-- otherwise type is not a record
RecurseAndCheck a (Cons (b :: m) r) = CNSat
-- Bellow lay a staple piece.
-- I want to say that any * type is a Record iff it is a * type generated by Hlist,
-- and every element of it is * but of kind Pair Symbol *.
class (forall t p (a :: HList) (l :: Pair Symbol *). RecurseAndCheck p a)
=> Record a
-- This what I see grants big potential of reuse. Something like AcyclicGraph can be established by checking
-- whether some regular Graph has nodes that point to each other.
The last bit is particularly tricky for me to handle. I want to say Some type is a record iff it is constructed by hlist and that every element is * that has kind Pair Symbol *
. It seems like it is very hard to do, and there has to be some way to say that variable must be * but it also must have specified kind. But I looked at many extensions and haven't found an obvious solution and neither can people on various forums.
So it all distils to a few key questions:
- How to specify that a variable must be
*
but have kindt
? - Does it look to you like System U?
- Why gch gives me an error about the presence of type family in quantified constraint in my case? That TF there is closed and injective, it is just a predicate, so is there really a reason to reject it?
- What can be computed on the right part of fat arrow and what can't be?
- Is it valid to say that t is in
*
t = Cons (MkPair "A" 0) ((Cons (MkPair "B" (Just "value")) End))
HList '[a :: Pair Symbol *, b :: Pair Symbol *, End]
- Do you know other places where I can ask these questions and get answers if you think that I annoy people here?