On 5 Jun 2015 22:13, "Matt Oliveri" <atma...@gmail.com> wrote:
> But that's not true. We can intersect (Int < 3) (Though I'd prefer to
> write it {z:Int | z < 3}.) With the evens, {z:Int | z % 2 == 0}, to
> get the type of evens less than 3: {z:Int | z < 3 && z % 2 == 0}. (I'm
> making up the syntax for predicates.)
These are intersections of the refinement, not intersection types like:
String /\ Int.
Where you showed a function as the intersection of function types, thats a
full intersection type requiring complex unification with expansion
variables.
> We can even intersect types that are refinements of incompatible
> unrefined types, and get the empty type. Like the intersection of Int
> and Float is empty. Maybe that's the part you don't like, where we're
> not just taking conjunctions of predicates. But you can see that at
> least within a given unrefined type, conjunctions give us
> intersections.
The intersection of int and float is not empty, but is in fact a function
that can be passed either an int or float, but can only do
operations/functions available on both.
> > type-classes which are constraints on types give a mechanism through
with
> > refinement types can be implemented:
> >
> > (Integer a, LessThan a Three) => a
>
> Maybe I'm being dense here, but there's a very big difference between
> constraints on types and constraints on values, because types and
> values are not the same. Are you using the Haskell hack of encoding
> values as dummy types? If so, how do you connect these types to the
> actual runtime values? (I think you might've shown me this already,
> but I forgot.)
Yes, and you can lift constants to types, in Haskell using Peano numbers
and polymorphic recursion.
I am actually thinking of type classes for dependent types, where you end
up with value-classes?
Keean.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
