On 2 May 2015 03:44, "Matt Oliveri" <[email protected]> wrote:
> > You can have a global coherence check.
>
> Sure, but that's a crutch in this case. Depend on the order rather
> than a phantom type, and you don't need typeclasses or coherence at
> all for this.

Well I want to make sure it's a compile time property, hence a type.

> Here is the signature for union in my solution:
> union : forall (E:Type) (o:Order E),Set E o->Set E o->Set E o
>
> Arguments E and o are implicit. In fact E can be implicit for Set too:
> union : forall (E:Type) (o:Order E),Set o->Set o->Set o

What is o? Is it an implicit value? Do I really want orders being passed
around at runtime?  Doesn't Set need a type parameter for the type of the
object n the set?

> > Interestingly type-classes are related to Prolog clauses, where clause
heads
> > are like instance definitions and are globally unique. This is where
you go
> > if you follow the argument to it conclusion and get rid of first class
> > functions.
>
> I don't think anyone has made an argument that would get rid of first
> class functions if followed to its conclusion.

One of the arguments in the video was that type-classes with global
coherence represent a better way of dealing with function arguments. 95% of
the time it was better not to factor out the argument and make the function
dependent on it. This makes you wonder what a language that makes every
function get passed like a type-class, and the answer is you would get
something like Prolog, but Prolog also exchanges types for values, such
that Prolog clause head matching is more like a value-class. What is
interesting is that Prolog is not totally useless. Prolog programs should
have the same global structure properties that were presented as
preferential in the video.

Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to