Sunday, October 06, 2013

[davsfkrm] Assert not an infinite data structure

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.)

1 comment:

Warbo said...

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

As 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