How Higgledy is working?

Learn
#1

Thans to @danidiaz, I’ve discover the Higgledy package.
It claims that it can make a HKD from a plain record.

When we work with higher-kinded data, we find ourselves writing types like:

data User f
  = User
      { name :: f String
      , age  :: f Int
      , ...
      }

This is good - we can use f ~ Maybe for partial data, f ~ Identity for complete data, etc - but it introduces a fair amount of noise, and we have a lot of boilerplate deriving to do. Wouldn't it be nice if we could get back to writing simple types as we know and love them, and get all this stuff for free?

data User
  = User
      { name :: String
      , age  :: Int
      , ...
      }
  deriving Generic

-- HKD for free!
type UserF f = HKD User f

Is it too good to be true ? I even don’t understand how it could work. Could someone explain please ?

#2

Haven’t you answered your own question at Transformative type families? It seems to be the same implementation as GHKD_ in the Higgledy docs.

#3

Possibly, but without being aware of it :wink:
Are transformative type families already working and is that Higgledy works ? (I had quick look but couldn’t see how it work, thus the question).

(Indeed, the two posts are related but I thought it’ll be better to make two separate posts).

#4

Are transformative type families already working and is that Higgledy works ?

Seems to be. Look at the definition of type family GHKD_. It’s the same as what you intended your F to be.

Transformative type families
#5

Fair enough. When did that happen ?
Was it type families feature from the start, or is in a new feature.
Unless it’s just a trick which happen to work.

Whichever way, that’s pretty cool.

#6

I think it’s simply a consequence of how type families and Generic work. I agree it’s pretty cool! I had never considered such a thing until your post.

3 Likes