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)
-}
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
