[MLton] Catching redundant pattern matches
Matthew Fluet
fluet@cs.cornell.edu
Mon, 13 Dec 2004 16:42:10 -0500 (EST)
> > Also, is your redundant case inside the body of an (unused) functor?
> > It turns out that we perform match compilation (and discover
> > exhaustive/redundant matches) on the defunctorized program.
> ...
> > This is probably reason enough to move the match compilation into
> > the elaborator.
>
> One reason we do match compilation after defunctorization is because
> of exception aliasing. I guess other implementations just assume
> exceptions aren't aliased, which generates redundant tests in some
> cases (not that this really matters for performance).
>
> Not warning about matches in unused functors is clearly a bug.
> Perhaps the right solution is to do match compilation in the
> elaborator just for the purposes of warnings, and then do match
> compilation after defunctorization to generate code. It is
> duplication of work, but may not be too costly.
John Dias (@ Harvard) has been studying the Definition, and we were
discussing that the Definition's allowance of inconsistent specifications
can lead to truly bizzare situations. For example:
signature SIG =
sig
datatype t = T
end
functor F1 (Str : SIG where type t = int) =
struct
open Str
fun isT (i : int) : bool =
case i of
T => true
| _ => false
end
This would appear to be type correct with respect to the Definition,
although there is no way to construct a structure matching
SIG where type t = int. T is a constructor, with type int.
It would appear that the following is also correct:
functor F2 (Str : SIG where type t = int) =
struct
open Str
fun isT (i : int) : bool =
case i of
T => true
| 42 => true
| _ => false
end
Andreas Rossberg's "Bugs & Defects" mentions this problem, without giving
a clear solution. When dealing with "int", MLton always assumes that the
matches are non-exhaustive, so demands a wild-card match. A related
problem is the following:
datatype u = U of bool
functor F3 (Str : SIG where type t = u) =
struct
open Str
fun isT (u : u) : bool =
case u of
T => true
| U b => b
end
Finally, I will note that MLton's -show-basis isn't always very
informative when forming inconsistent signatures. If I add the signatures
signature SIG' =
sig
datatype v = V
end where type v = int
signature SIG'' =
sig
type w
end where type w = int
to the above declarations, then -show-basis yields:
datatype u = U of ?.bool
functor F1 (S: SIG
where datatype t = ?.int32)
: sig
datatype t = T
val isT: ?.int32 -> ?.bool
end
functor F2 (S: SIG
where datatype t = ?.int32)
: sig
datatype t = T
val isT: ?.int32 -> ?.bool
end
functor F3 (S: SIG
where datatype t = u)
: sig
datatype t = T
val isT: u -> ?.bool
end
signature SIG =
sig
datatype t = T
end
signature SIG' =
sig
datatype v = V
end
signature SIG'' =
sig
eqtype w = ?.int32
end
which doesn't seem to describe SIG' correctly.