#6018: Injective type families
----------------------------------------+-----------------------------------
Reporter: lunaris | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: TypeFamilies, Injective | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
----------------------------------------+-----------------------------------
Comment(by mokus):
An interesting use case is type-level co-naturals using -XDataKinds (which
I'm using as the "height" type index for an experimental 2^k-tree
implementation):
{{{
data Nat
= Zero
| Suc Nat
data CoNat
= Co Nat
| Infinity
type family Succ (t :: CoNat) :: CoNat
type instance Succ (Co n) = Co (Suc n)
type instance Succ Infinity = Infinity
}}}
Succ can't be a constructor, because then Succ Infinity /~ Infinity. Succ
as a type family half-works, but you end up needing
(logically-)unnecessary type annotations all over the place because GHC
doesn't know that Succ n ~ Succ m => n ~ m. It might be possible to
devise some kind of type-level bisimilarity constraint, but I suspect it
would actually increase the need for type annotations rather than decrease
it.
I've also tried an alternate definition of the tree type using "Pred"
instead of "Succ", but that seems to lead to really bizarre types - it
accepts obviously non-flat trees at a type indicating that the tree's
height is zero (or actually, any CoNat I want), because it accepts the
existence of types such as "Pred (Co Zero)". Is this expected behavior
(e.g., due to the open-world assumption) or should I file a bug report on
that?
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6018#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
