search

obsidiansystems / dependent-map

Dependently-typed finite maps (partial dependent products)
Other
63 stars 33 forks source link

Poly-kinded DMap #3

Closed int-index closed 9 years ago

int-index commented 9 years ago

The error I'm getting is

        The first argument of ‘DMap’ should have kind ‘* -> *’,
          but ‘NComponent a’ has kind ‘N -> *’
        In the type signature for ‘components’:
          components :: Expr a -> DMap (NComponent a)

It was a surprise for me that DMap is not poly-kinded. Perhaps https://github.com/mokus0/dependent-sum/issues/3 is somewhat related.

mokus0 commented 9 years ago

As it stands right now, it cannot be poly-kinded - the type itself would not be well-kinded at anything other than (* -> *) -> *, because both the keys and the values must have kind . There is a variation I've experimented with before that can be kinded as `(k -> ) -> (k -> ) -> `, but is a bit clunkier to use in the usual case (it applies the first param to the keys and the second to the values).

I hadn't thought about the kind-level implications of that change, this is actually a pretty good case for moving that direction.

mokus0 commented 9 years ago

This is now on hackage as dependent-sum 0.3.* and dependent-map 0.2.*

int-index commented 9 years ago

Awesome!