On Sat, Jun 6, 2015 at 6:03 AM, Keean Schupke <[email protected]> wrote: > 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.
Unfortunately, based on the definition of Triangle you gave, this stuff still doesn't seem to make sense. How can you meaningfully test whether a type can represent triangles, for example? And why would you apply that test to a polygon, which is not a type? And why is "the question of whether a triangle is a type" so interesting? The answer still seems to be a resounding "No, triangles are not types." _What_ can be ((0,0),(10,0),(0,10)) but not [(0,0),(10,0),(0,10)]? Both of those data can be interpreted as right triangles, and neither of them are types. The key may be how you're thinking of lifting values to types. I saw a presentation of how to do logic-like stuff with path dependent types in Scala. It was horrible. If you're making a new language, why would you resort to hacks like that, and not--you know--actually put things from logic in your language? And the answer had better not be because you think it messes up the phase distinction, or static type resolution, because we can always just erase all the propositions and proofs. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
