Skip to content

Instantly share code, notes, and snippets.

Created Oct 7, 2012
What would you like to do?
Demonstration of the usefulness of NLong for type inference
I'm still in the experimentation stage and cannot completely explain/defend my design decisions.
The big picture is: this code is working as a polyvariadic version of generic-deriving. I've run
into the issue that my original email "seemingly inconsistent behavior for "kind-indexed" type
constraints in GHC 7.6" to the glasgow-haskell-users list is about when trying to add support
for representing indexed data types in a way that is 1) congruent with GHC's elaboration of
GADTs, and 2) uniquely (I think) enabled by the polyvariadism of my technique.
Like I said, I'm not certain about all of my design decisions. In particular, if you're wondering
why I am defining the W instances using the Nth type family, then I don't have a satisfying answer
for you. Simply, I get type errors (in instances of Generic) if I instead define instances of W by
directly matching on the ps argument. In fact, I get the same type errors that I've discussed in the
original email in this thread. That's why I lead with just NLong out of context; my need for it is
kind of circular from the perspective of these emails.
If you are still interested in more technical details than this gist provides, you might as well
dive into the library.
I'm totally available by email. Thanks for your time.
-- naturals
data Nat = Z | S Nat
-- indexes in the type list
type family Nth (n :: Nat) (ts :: [k]) :: k
type instance Nth Z (a ': as) = a
type instance Nth (S n) (a ': as) = Nth n as
-- represents an uncurried application of t
data family W (t :: k) :: [*] -> *
-- this instance of W handles one argument, there's infinitely many instances...
newtype instance W (t :: * -> *) ps = W1 (t (Nth Z ps))
asW1 f = (\(W1 x) -> x) . f . W1
-- the NLong class, which was (poorly) abstracted as NUnits in
class NLong (n :: Nat) (ts :: [*])
instance (ts ~ '[]) => NLong Z ts
instance (ts ~ (t ': tstail), NLong n tstail) => NLong (S n) ts
-- Rep/Generic are like generic-deriving, except for the kind polymorphism
type family Rep (t :: k) :: [*] -> *
class Generic (t :: k) where
toRep :: NLong (CountArgs ('KindProxy :: KindProxy k)) ps => W t ps -> Rep t ps
frRep :: NLong (CountArgs ('KindProxy :: KindProxy k)) ps => Rep t ps -> W t ps
-- CountArgs, and KindProxy are the same as from
OK, with all that in place, the ghci query
*> :t atW1 $ \x -> frRep (toRep x) `asTypeOf` x
which reads as "at kind * -> *, convert to the representation and back", returns the type
Generic (* -> *) t => t a -> t a .
If the NLong constraints weren't on toRep and frRep, that same expression would have the inferred type
Generic (* -> *) t => t (Nth * 'Z ps) -> t (Nth * 'Z ps) ,
which ultimately leads to "ambiguous type variable ps0" in the user's code.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment