On Sun, May 3, 2015 at 6:59 PM, Keean Schupke <[email protected]> wrote:
> 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.
You _can_ implement an HM type checker that way, if it's really just
HM. (E.g., no modules.) Still, no-one does that.
Try the following code in OCaml, or analogous code in whatever
language w/ generic types you have on hand:
(fun (f:'a->'a->'a)->f) (fun x->x)
Error: This expression [x] has type 'a but an expression was expected of type
'a -> 'a
The type variable 'a occurs inside 'a -> 'a
Now how could it know that expression is nonsense (without
equirecursive types at least) without knowing what 'a is? Only one
explanation: it type checked it.
>> >> 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.
Either we are having a hilarious misunderstanding, or one of us has
learned type checkers all wrong. :)
Maybe this helps:
Abstract types means having variables in types, such that you can
check *expressions* at those abstract types.
> 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,
You have not defined any functions...
>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'.
Right. So you get:
h :: forall a . a -> a
> When I get to the main program:
>
> main = f g 1 2 3
You get a type error because you gave f too many arguments.
> No type variables are allowed to be unknown, because they do not exist
> outside of main.
What do you mean?
> There is no way for main to pass a value of unknown type to
> any function,
Well you're mixing up runtime and compile time in that sentence. There
_is_ a way to use an expression of unknown type as an argument. It'll
just screw up if you run it:
main = f (hd []) 3
(In Haskell, this might not screw up, depending on the definition of f.)
> 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.
What do you mean?
> 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)
I'd say this is a peculiarity of typeclasses, not a general principle
for abstract types. The reason the un-annotated code doesn't compile
is not that the intermediate type is unknown, but that it can't infer
an instance. Not even at runtime. The code is ambiguous.
>> 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.
You might not need that part. Yeah, actually I cheated. The staging
literature seems interested in computing values at compile time. I
thought it went without saying that it could be adapted for computing
types at compile time. The difference remaining from usual type-level
functions would be that the stage separation guarantees that types "in
the mode" can be statically resolved.
> When typeclasses already have static resolution, why would I want yet
> another typeclass like mechanism?
Because you could add "existentials", and still have typeclasses over
types with existentials, and add instance arguments, and add dependent
types, and add everything but the kitchen sink, and you'd still know
that types "in the mode" would be known at compile time.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
