Can I compute on right part of a fat arrow?

Learn
#1

Let’s assume you have this code:

data HList :: [*] -> *  where
   Cons :: p -> HList a -> HList (p ': a)
   End :: HList '[]

-- convinience to not write explicit signature
class CBottom
type CSat = () :: Constraint
type CNSat = CBottom

type ConstStr = '[Char]
data Pair a b where
   MkPair :: a -> b -> Pair a b

-- Check if hlist have all elements of type Pair '[Char] Type
type family RecurseAndCheck a (b :: HList t) where
   RecurseAndCheck a End = CSat
   RecurseAndCheck a (Cons (b :: a) r) = RecurseAndCheck a r 
   RecurseAndCheck a (Cons (b :: m) r) = CNSat

-- Any hlist that is constructed from Pairs of (ConstStr, Type) is a TypeClass
class (forall t p (a :: HList t) . RecurseAndCheck (Pair ConstStr p) a) 
   => TypeClass a where
   retrieve :: a -> (s :: ConstStr) -> Pair a s

Unfortunately, compiler shows me a horrible error:
Occurs check: cannot construct the infinite kind: t ~ a : t • In the second argument of ‘RecurseAndCheck’, namely ‘(Cons (b :: a) r)’

So two questions:

  • What can I do to vanquish the error?
  • Do you see anything awkward in this code?
#2

I think both arguments of the type family need to be types. In your case the second argument (c :: HList t) is a value not a type.

You can do this, but it still feels awkward:

type family RecurseAndCheck a bs where
  RecurseAndCheck a (HList '[]) = CSat
  RecurseAndCheck a (HList (a : bs)) = RecurseAndCheck a (HList bs)
  RecurseAndCheck _ _ = CNSat

-- Any hlist that is constructed from Pairs of (ConstStr, Type) is a TypeClass
class (forall t p . RecurseAndCheck (Pair ConstStr p) (HList t)) 
   => TypeClass a where
   retrieve :: a -> (s :: ConstStr) -> Pair a s

P.S. I would define type CNSat = Int ~ Bool, then you cannot accidentally make an instance.

1 Like
#3

Thank you for response, I am still in a learning phase and your remarks are helpful.
Unfortunately, the stopper is now Quantified predicate must have a class or type variable head and it seems to be a major hindrance here (despite my ignorance, of course). Doing troubleshooting, I found at gitlab a discussion that mentioned this error and it looks dormant. So it seems like it is not possible to compute on the left side of the arrow, even with closed type families, is this statement correct?

Oh, yes! It is definitely better.

1 Like
#4

You’re doing some quite advanced Haskell for someone in a learning phase :slightly_smiling_face:. I feel like I am only a few steps ahead of you in the learning process, so I can’t give any definitive answers.

I only really focused on fixing the error. Now that I’m reading it a bit better the quantification seems strange. The left side of the “fat arrow” is not connected to the right side at all. Now it is saying something like "If all heterogeneous lists consists of only pairs then you can make an instance for TypeClass". But clearly you can come up with some HLists that do not contain only those specific pairs. So you probably want something more like:

class (forall p . RecurseAndCheck (Pair ConstStr p) (HList t)) 
   => TypeClass t where
   retrieve :: HList a -> (s :: ConstStr) -> Pair a s

But this is still not really what you want (and it will still give the same error) because of that forall p. You probably want to define RecurseAndCheck slightly differently:

type family RecurseAndCheck bs where
  RecurseAndCheck (HList '[]) = CSat
  RecurseAndCheck (HList (Pair ConstStr _ : bs)) = RecurseAndCheck a (HList bs)
  RecurseAndCheck _ _ = CNSat

This is less general, but it allows you to completely remove the foralls from the left side of the “fat arrow”. But at this point I’m also running out of ideas because the type of retrieve: a -> (s :: ConstStr) -> Pair a s does not really make sense to me. Can you explain it a bit more?

1 Like
#5

Sure. I thought that it’s how term level strings are represented at the type level. I just found out that mature haskellres call it Symbol, so I’ll google that. The idea was to construct a record with functions, basically.

To clarify a bit more, I made TypeClass type class to simplify the signature of a particular function.
My intention was to try to implement ‘nominal instances’ as ‘things that carry implementation’ so for example you could create multiple records with functions and later use them in context at will. Can’t make up convincing examples of how it would look like, sorry :pleading_face:. Anyway, I was mostly trying to stretch it for fun.