On 4/16/12 5:40 PM, Geoffrey Irving wrote:
> On Mon, Apr 16, 2012 at 1:41 PM, Jonathan S. Shapiro<[email protected]>
wrote:
>> It's merely a choice of how to interpret the notation. So in the end, I'm
>> not sure why the notation
>>
>> map :: (x -> y) -> List x -> List y
>>
>> needs to change here when we intend to be polymorphic over effects and
>> constantness.
>>
>> The place that needs to change when we want explicit instantiation is the
>> internal type of map, where we need to document our intention.
>
> After reading this first I was a bit queasy about "lying to the user",
It's not lying, it's just underspecified. Consider for your amusement the
following syntax instead:
a -{Const}-> b a function implemented via compile-time constant
a -{Closure}-> b a function implemented via closure
a -{x}-> b a function polymorphic in implementation sort
This is the sort of trick that DDC uses for their effect system. A similar
system has been proposed for Haskell-alike languages that want to be
explicit about the distinction between (necessarily)strict and
(possibly)non-strict functions. There's no reason why the "a -> b" syntax
cannot be simply a shorthand for a -{x}-> b where x is a fresh
metavariable and subject to whatever unification and generalization the
type checker does. Indeed, that'd be a good way to go about things since
it allows reducing verbosity when the type can be inferred from usage.
> I do think there would be annoying syntax required when returning
> functions or packing them into data structures, since you'll end up
> having to explicitly say what type you want stored in many cases.
> This is probably inevitable, though.
Possibly, though no more so than when being explicit elsewhere, I don't
think. In particular, if you consider constness something that a
(meta)variable can range over, as above, then you can effectively express
types like "this function returns a function of the same implementation
sort as its argument"--- without needing the definition to be monomorphic
in the implementation sort of its argument. In practice, you'll probably
have/want to specialize the function for Const and Closure arguments, but
that's no different than any other form of type-based specialization.
Constant functions can be represented by code pointers, closures can be
represented by, well, closures; how's that any different in principal than
Int32 vs Int64?
--
Live well,
~wren
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
