[Haskell-cafe] Type families and GADTs in 6.9
Dan Doel
dan.doel at gmail.com
Sat Apr 12 01:06:45 EDT 2008
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
More information about the Haskell-Cafe
mailing list