[Haskell-cafe] Re: Type families and GADTs in 6.9

[Dan Doel]

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