On 3 May 2015 at 23:38, Matt Oliveri <[email protected]> wrote:
>
> Nope, just C++, I think. It's an anti-modular way to type check.
>

HM type checkers work like this too. I have implemented a few.


> >> Yes, but at this point, I'm more concerned you don't know what type
> >> abstraction is than that you think implicit arguments should be
> >> abandoned for this reason.
> >
> > I think it would be good if you could explain what you mean by
> > type-abstraction, as I think I am thinking of something slightly
> different.
>
> Variables in types, such that you can check programs at those abstract
> types.
>

I think you are not fully thinking through the process of type checking.

Lets say I have some functions:

f :: forall a b . a -> b -> b
g :: forall a b .  a -> b -> a

Now I can type check these polymorphic function definitions on their own
with the type variables no problem, but lets say I now want to type check:

h x = f g x

To work out the type of 'h' I need to instantiate and unify the types of f
and g with the type variable for the variable 'x'.

When I get to the main program:

main = f g 1 2 3

No type variables are allowed to be unknown, because they do not exist
outside of main. There is no way for main to pass a value of unknown type
to any function, which means all the unknown type variables that are now
linked together by the unifications of the type labels on the abstract
syntax tree, are now grounded. All of them, without fail. It is an error is
any are unspecified. The easiest way to see this is to consider:

show (read string)

read reads a string to a value for all types, show converts any type to a
string. This program is ill-types, because the type output by read is not
determined. But this is okay:

show (read string :: Int)

Hmm, well it can't be much worse than C++ templates. And really, I bet
> it's actually much better. Keep in mind that you could try to add a
> statically-resolvable version of typeclasses on top of this mechanism.
>

Its the code quoting mechanism that I don't like.

When typeclasses already have static resolution, why would I want yet
another typeclass like mechanism?


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

Reply via email to