[Haskell-cafe] working through "Part I: Dependent Types in Haskell"
Andres Löh
andres at well-typed.com
Mon Apr 27 12:31:28 UTC 2015
Hi.
> init' :: Vector a ('S n) -> Vector a n
> init' (x1 :- Nil) = Nil
> init' (x :- xs) = x :- (init' xs)
You need to pattern match further on `xs` in order to make clear that
you require it to not be `Nil`. The type checker doesn't look at the
first case in order to conclude that you've already ruled that out.
So e.g.
init' (x :- xs @ (_ :- _)) = x :- (init' xs)
works.
Cheers,
Andres
--
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com
Registered in England & Wales, OC335890
250 Ice Wharf, 17 New Wharf Road, London N1 9RF, England
More information about the Haskell-Cafe
mailing list