Talk:Generalised algebraic datatype
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
Sort of a practical question here...
data Empty
data NonEmpty
data List x y where
Nil :: List a Empty
Cons:: a -> List a b -> List a NonEmpty
safeHead:: List x NonEmpty -> x
safeHead (Cons a b) = a
If I try to compile the above code with all warnings on, I get a pattern match non-exhaustive warning on safeHead because I'm not matching on Nil. This is pretty annoying. Is this the kind of thing that can easily be fixed? Can the compiler somehow magically recognise that if I've got a List x NonEmpty, then the only patterns to match on are Cons (because those are the only ones that return List x NonEmpty)? Or is there some theoretical barrier to this?