The question that I am pondering is whether I can bridge the two by adding type-safe casting operations to the definitions of types. Perhaps by using some form of type-class, or concept.

Consider the following function grow_list which takes a list and appends an element to it a specified number of times:

define grow_list : (a:list x:value n:uint) -> (b:list)
{
  [[dup [append] dip] dip dec] [dup neqz] while pop pop
}

If the implementation is meaningless to you, it isn't very important, but it is pretty much the same as Joy.

The question is, should I express the postcondition as part of the type expression? The postcondition can be expressed in pseudo-code:

[{ b size } { a size n + } eq]

1. should the type system capture postconditions and other constraints
2. if so then what should the mechanism be for expressing constraints?

define grow_list : (a:list x:any n:int)->(b:list) 
  <: [{ b size } { a size n + } eq]
{
   ...
}