Oh! I had assumed that it was already considered rude to expose a
non-exhaustive function to the outside world:
you mean, as in: head, tail, fromJust, ..?-)
whether exposing or using those is considered rude or not, the type
system has nothing to tell us about their not handling some inputs,
and if you get them from precompiled libraries, you don't see the
compiler warnings, either.
one could turn that promise into a type-checked guarantee by using
explicit sum types (and thus structural rather than name-based typing),
but that gets awkward in plain haskell.
I don't think the choice of whether you label your variants with names
or with numbers (in1, in2, in3...) has anything to do with the choice of
whether you require your cases to be exhaustive or not.
i was talking about name-based (as in: this is the sum type named List)
vs structural (as in: this is the sum type build from Cons and Nil) typing.
the former hides (in-)exhaustiveness from the type system, the latter
exposes it.
consider the example code below, where the type system catches the
non-exhaustiveness of g, where the sum structure of its parameter is
exposed, but has nothing to say about f, where the sum structure is
hidden behind a type name.
claus
{-# OPTIONS_GHC -fallow-overlapping-instances #-}
{-# OPTIONS_GHC -fglasgow-exts #-}
{- our own, nameless sum type with injection and unpacking -}
infixr :|
data a :| b
data a :< b = Inj a deriving Show
class Inj a b where { inj :: a -> a:<b ; out :: a:<b
-> a }
instance Inj a a where { inj a = Inj a ; out (Inj a) = a }
instance Inj a (a:|b) where { inj a = Inj a ; out (Inj a) = a }
instance Inj a b => Inj a (c:|b) where { inj a = Inj a ; out (Inj a) = a }
{- a product type of nested pairs, with selection -}
class Sel a b where sel :: b -> a
instance Sel a a where sel a = a
instance Sel a (a,b) where sel (a,_) = a
instance Sel a b => Sel a (c,b) where sel (_,b) = sel b
{- to match, supply a product of functions covering the sum -}
match :: (Inj x xs, Sel (x->b) fs) => x:<xs -> fs -> b
match x fs = sel fs (out x)
{- example A: nameless sum -}
type Sum = String :| Char :| Bool
g y = match y (\s->s::String,
(\c->c:""
))
-- ,(\b->if b then "1" else "2")))
{- example B: named sum -}
data NamedSum = S String | C Char | B Bool deriving Show
f :: NamedSum -> String
f (S s) = s
f (C c) = c:""
-- f (B b) = if b then "1" else "2"
{- testing -}
main = do
putStrLn $ g (inj "hi" :: String:<Sum)
putStrLn $ f (S "ho" :: NamedSum)
putStrLn $ g (inj 'x' :: Char:<Sum)
putStrLn $ f (C 'y' :: NamedSum)
putStrLn $ g (inj False :: Bool:<Sum)
putStrLn $ f (B True :: NamedSum)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
