When & Where: 12:30pm, Friday, March 10, 2006, Room 200 AKW
Abstract:
Dance is a high-level declarative language embedded in Haskell for controlling robots. The design of dance must accommodate the constraints of bodypart movements. For example, a bodypart can not perform more than one actions at the same time. Our previous solution was to perform dynamic checks to detect such situations. However, dynamic checks incur runtime overhead and increase the complexity of the language interpreter.
In this talk, I will present a static and concise solution to this problem using Dependent Type Programming. This solution is made possible with some features of the Haskell type system, such as type class and GADT. First, bodyparts are lifted to the type level and defined inductively. Next, several type classes are introduced to express logical relations of bodyparts, enforcing movement constraints. Finally, using GADT, proper constraints are linked with dance constructors to prevent unsafe dance programs.