On 6 Jun 2015 9:26 am, "Matt Oliveri" <[email protected]> wrote:
> 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.
f : forall a. (Triangle a, Right a) => a -> a
The question of whether a triangle is a type is an interesting one it can
be:
((0,0),(10,0),(0,10))
And is can not be:
[(0,0),(10,0),(0,10)]
I think of the type classes as general predicates on types, and you can
'lift' a value to a type using path dependent types. So consider:
let a = getPolygon in if Triangle a then ... else ...
Reading 'a' at runtime it is a general polygon however after applying the
'if' test we know it is a triangle in the 'then' branch and not a triangle
in the 'else' branch. So conditional branches can lift values to types in a
member/not member way.
> 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.
Consider:
f : Int /\ Float -> String
> > 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.
Sorry, it was a terminology question. Would you call type - classes applied
to dependent types value-classes? In any case I am still using type -
classes, just creating dictionaries from conditional branches.
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
