Dafny: Generic method on a base type and a subset type?

Question

Can I define a generic method on a base type and subset type?

For example, we might later use the generic function by having

• T0 be the sets of integers, and
• T1 be the non-empty sets of integers

I image something like:

method MergeAndTouch<T0, T1>(Touch: (T1,T1)->bool, Plus: (T0,T0)->T0, unit: T0, xs: seq<T1>, a: T1)
  requires T0 >= T1 // NOT ALLOWED
  requires Reflexive(Touch)
  requires Symmetric(Touch)
  requires IsAssociative(Plus)
  requires IsUnital(Plus, unit)
  requires forall i:T1, j:T1 :: Touch(Plus(i, j), i) && Touch(Plus(i, j), j)
  requires forall i:nat, j:nat :: i < j < |xs| ==> !Touch(xs[i], xs[j])
{
// code goes here
}

I need this to exclude things like the empty set from the generic Touch while still having things like the empty set as the unit for operations such as FoldLeft.

Answer 1

In this case subset language feature can be used. This is how it will look like

ghost function NonEmptySetExample<T(00)>() : (r: set<T>)
{
    var t : T :| true ; {t}
}

type NonEmptySet<T(00)> = s : set<T> |  s != {} 
     ghost witness NonEmptySetExample<T>()

You can use set methods (in here) on NonEmptySet.

ghost function Test<T(00)>(t: NonEmptySet<T>) : T 
{
    var x : T :| x in t; x
}  

Additionally you can define method taking set as argument and call with NonEmptySet

method TypeMethod<T>(s: set<T>) 
{
}

method CallTypeMethodOnSubSet<T(00)>(t: NonEmptySet<T>)
{
   TypeMethod(t);
}

Note: T(00) means type parameter itself is non empty.