On Sat, Jun 6, 2015 at 6:03 AM, Keean Schupke <[email protected]> wrote: > 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 still haven't told me is whether "a" from your examples is itself a type. If so, what are its elements? If not, how can you apply a type class to it? Without this information, you cannot expect me to make much sense of this. Maybe it'd help if you actually showed me the definition of Triangle. >> 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 Consider it considered. What's the point? Do you still deny that (Int /\ Float) can be defined as empty? >> > 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? You mean type classes applied to values? If they're applied to dependent types, well those are still types, so they should still be called type classes. I don't know if dependent type systems let you apply something like type classes to values. It would make sense if they did. I don't know what that's called. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
