Future of roles for GADT-like type variables?

Author of the roles system here. I’m aware of no ideas that will move us forward in this direction. The problem is that we’d need to check a delicate property in order to ensure that the coercion is safe. Specifically, we want to be able to coerce e.g. HList [Age, Int, String] to HList [Int, Age, String] but not to HList [String, String, Int] (or an HList with something other than three elements). (I’m assuming newtype Age = MkAge Int here.) Pulling this off would require some Very Glorious role-like system — capable of describing exactly what coercions would be safe for such a GADT — and I don’t know of any work toward creating such a system.

The reason the data family approach works is that GHC can see that HList [Age, Int, String] is really the same as (Age, (Int, (String, HList '[]))), and then it knows tuples well enough to do the rest of the work.

Sorry to have no encouragement here, but this seems well beyond what we can do now.

Leave a Comment

Hata!: SQLSTATE[HY000] [1045] Access denied for user 'divattrend_liink'@'localhost' (using password: YES)