On Sat, Jun 6, 2015 at 2:24 AM, Keean Schupke <[email protected]> wrote:
> On 5 Jun 2015 22:13, "Matt Oliveri" <[email protected]> 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.
This is what I was saying about only necessarily having intersections
among the refinements of a given unrefined type. You are right that
String intersect Int is not staying within a single unrefined type.
> Where you showed a function as the intersection of function types, thats a
> full intersection type...
True.
> ...requiring complex unification with expansion variables.
Maybe. In that case, you might prefer:
{f:Triangle->Triangle | forall t,Right t->Right (f t)}
as the type of a triangle transformer that preserves rightness.
>> 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.
What you describe sounds like the intersection of functions on int
with functions on float. This does not tell us what the intersection
of int and float is. There are multiple subtype orders that are
sensible. I was thinking of int and float as unrelated, so their
intersection is empty.
>> > 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.
OK, but that's not the part I'm asking about. I don't think. Given
some machinery for numbers encoded as types, how do you now use that
to prove things about programs that work with actual runtime numbers?
> I am actually thinking of type classes for dependent types, where you end up
> with value-classes?
You're asking me what you're actually thinking of? I don't know. Maybe
Sandro knows. Have you seen his email about what Habit does? It does
kind of look like what you've shown.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
