In Haskell, support an assertion that a given expression is not an infinite data structure. Of course, this is trivially reduceable to the impossible Halting Problem, so we seek approximations: determine whether the assertion definitely holds, definitely fails, or the compiler can't figure it out.
Could be done at compile-time, or possibly at runtime when there is more information.
Inspired by debugging with Debug.Trace: we don't want printing an expression to hang the program. (And in particular debugging a compiler compiling a program with data or type recursion.)
I've done this before using type-level datastructures, although it only works on one datastructure at a time. See http://chriswarbo.net/index.php?page=news&type=view&id=admin-s-blog%2Fsafety-through-types
ReplyDeleteAs an example, we can model finite polymorphic lists:
-- Nil has a type but no data
data Nil t = Nil
-- Cons takes a type-constructor l, which it instantiates with its element type
data Cons l t = Cons t (l t)
-- Implementing this class implies that a datastructure is finite
class FiniteList l where
toList :: l t -> [t]
-- Empty lists are finite
instance FiniteList Nil where
toList Nil = []
-- Cons is finite if its tail is finite
instance (FiniteList l) => FiniteList (Cons l) where
toList (Cons x xs) = x : toList xs
This is pretty much a literal translation of lists to the type level, using types as constructors and classes as types. The difference is in the semantics: class instances aren't lazy, they're evaluated (unified) eagerly at compile-time. For the compiler to accept a FiniteList value, it must be able to find a Nil in that value.
Another problem with this approach is that classes are open; I could easily break it by defining:
instance FiniteList ([]) where
toList l = l