Type families and GADTs in 6.9
Hello, I've been playing around with type families off and on in 6.8, but, what with the implementation therein being reportedly incomplete, it's hard to know what I'm getting right and wrong, or what should work but doesn't and so on. So, I finally decided to take the plunge and install 6.9 (which, perhaps, isn't yet safe in that regard either, but, such is life :)). But, when I loaded up one of my programs, I got a type error. The subject is inductively defined tuples: ------------------------------------- {-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls, TypeOperators #-} data Zero data Succ n data Nat n where Zero :: Nat Zero Succ :: Nat n -> Nat (Succ n) data FZ data FS a data Fin fn n where FZ :: Fin FZ (Succ n) FS :: Fin fn n -> Fin (FS fn) (Succ n) f0 = FZ f1 = FS f0 f2 = FS f1 -- ... etc. data Nil data t ::: ts type family Length ts :: * type instance Length Nil = Zero type instance Length (t ::: ts) = Succ (Length ts) type family Lookup ts fn :: * type instance Lookup (t ::: ts) FZ = t type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn infixr 4 ::: data Tuple ts where ZT :: Tuple Nil (:::) :: t -> !(Tuple ts) -> Tuple (t ::: ts) {- This type signature gets complained about in 6.8, but it seems like a sensible one: proj :: (Length ts ~ n) => Fin fn n -> Tuple ts -> Lookup ts fn Indexing the tuple by its length is also an option (which works). In any case, the code doesn't even work with the lenient 6.8 signature: -} proj :: Fin fn n -> Tuple ts -> Lookup ts fn proj FZ (v ::: vs) = v proj (FS fn) (v ::: vs) = proj fn vs ------------------------------------- The overall goal being Haskell-alike tuples with a single projection function that works for all of them, without having to use template haskell for instance (fst = proj f0, snd = proj f1, etc.). However, proj results in a type error: Occurs check: cannot construct the infinite type: t = Lookup (t ::: ts) fn In the pattern: v ::: vs In the definition of `proj': proj FZ (v ::: vs) = v Oddly (to me), if I reverse the clauses, the compiler doesn't complain about the FS case, still complaining about FZ. Now, my thought process here is that the pattern match against FZ (the value) requires fn to be FZ (the type), which should tell the compiler to solve "t ~ Lookup (t ::: ts) FZ" which is, of course, the first instance above. Am I doing something wrong, or have I bumped into as-yet-unimplemented functionality? Thanks for your time and help. -- Dan
The length calculation looked complicated. So I reformulated it as a comparison using HasIndex. But ghc-6.8.2 was not inferring the recursive constraint on proj, so I split proj into proj_unsafe without the constraint and proj with the constraint checked only once. I also renamed ZT to Nil to be more consistent.
-- works in ghc 6.8.2 {-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls, TypeOperators #-}
data FZ data FS a
data Fin fn where FZ :: Fin FZ FS :: Fin fn -> Fin (FS fn)
f0 = FZ f1 = FS f0 f2 = FS f1 -- ... etc.
data Nil data t ::: ts
infixr 4 :::
data Tuple ts where Nil :: Tuple Nil (:::) :: t -> !(Tuple ts) -> Tuple (t ::: ts)
data HTrue
type family Lookup ts fn :: * type instance Lookup (t ::: ts) FZ = t type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn
type family HasIndex ts fn :: * type instance HasIndex (t ::: ts) FZ = HTrue type instance HasIndex (t ::: ts) (FS fn) = HasIndex ts fn
{-# INLINE proj #-} proj :: (HasIndex tsT fnT ~ HTrue) => Fin fnT -> Tuple tsT -> Lookup tsT fnT proj = proj_unsafe where proj_unsafe :: Fin fnT -> Tuple tsT -> Lookup tsT fnT proj_unsafe (FS fn) (_v ::: vs) = proj_unsafe fn vs proj_unsafe FZ (v ::: _vs) = v proj_unsafe _ Nil = error "Cannot proj Nil in proj_unsafe"
fst' :: (HasIndex ts FZ ~ HTrue) => Tuple ts -> Lookup ts FZ fst' = proj f0
snd' :: (HasIndex ts (FS FZ) ~ HTrue) => Tuple ts -> Lookup ts (FS FZ) snd' = proj f1
pair :: Tuple (Char ::: (() ::: Nil)) pair = 'a' ::: () ::: Nil
q1 :: Char q1 = fst' pair
q2 :: () q2 = snd' pair
{- This won't compile
q2 :: () q2 = snd' ('a' ::: Nil) -}
On Saturday 12 April 2008, ChrisK wrote:
The length calculation looked complicated. So I reformulated it as a comparison using HasIndex. But ghc-6.8.2 was not inferring the recursive constraint on proj, so I split proj into proj_unsafe without the constraint and proj with the constraint checked only once. I also renamed ZT to Nil to be more consistent.
Ah, well, in fact, you can also structure things this way: ------------------------------ data Tuple ts n where Nil :: Tuple Nil Zero (:::) :: t -> Tuple ts n -> Tuple (t ::: ts) (Succ n) proj :: Fin fn n -> Tuple ts n -> Lookup ts fn -- proj is the same as my original mail ------------------------------ That ensures that a tuple of size n is indexed by the finite set of size n. The two are a natural fit for one another, since there are as many elements in the tuple as there are in the finite set. This actually works on 6.8.2 (modulo having to tell GHCi what result type it ought to get in some cases, since it thinks there is no Show instance for Lookup (Int ::: Nil) FZ :)), and gives type errors if you try to do, say 'proj f2 ('a' ::: 'b' ::: Nil)': f2 :: Fin (FS (FS FZ)) (Succ (Succ (Succ n))) tuple :: Tuple (Char ::: Char ::: Nil) (Succ (Succ Zero)) => Succ (Succ (Succ n)) ~ Succ (Succ Zero) -- no can do My main confusion was that none of this works in 6.9, seemingly because the pattern match against FZ in proj fails to refine the type variable fn to FZ, which is necessary to solve the equation 't ~ Lookup (t ::: ts) fn', so instead it tells me I'm asking for an infinite type. However, the type checker not figuring out that Succ n ~ Length (t ::: ts) implies that n ~ Length ts in the recursive call is, I think, the problem I was having with the original alternate signature. I suppose it's less trivial than HasIndex, but you say it didn't like that either. It'd be interesting to know if that sort of thing will be possible in 6.10, or if it's unreasonable to expect that to work. Cheers. -- Dan
Dan,
I've been playing around with type families off and on in 6.8, but, what with the implementation therein being reportedly incomplete, it's hard to know what I'm getting right and wrong, or what should work but doesn't and so on. So, I finally decided to take the plunge and install 6.9 (which, perhaps, isn't yet safe in that regard either, but, such is life :)). But, when I loaded up one of my programs, I got a type error. The subject is inductively defined tuples: [..] However, proj results in a type error:
Occurs check: cannot construct the infinite type: t = Lookup (t ::: ts) fn In the pattern: v ::: vs In the definition of `proj': proj FZ (v ::: vs) = v
Sorry, but looks like a bug in 6.9 to me. Could you add it to the GHC bug tracker? Thanks, Manuel
participants (3)
-
ChrisK -
Dan Doel -
Manuel M T Chakravarty