Re: [scala] usefulness of OOP

[Shelby]

I am replying to the following linked post from a thread, which is on
the old version of this mailing list before it was moved to Google
Groups. I could not find a copy of the following linked thread here in
Google Groups.

http://scala-programming-language.1934581.n4.nabble.com/scala-usefulness-of-OOP-tp2000320p2000324.html

<quote author="Jon Harrop">
The overhead of the module-related code may be constant but the
overhead of
your unnecessary explicit type definitions certainly is not and that
does not
afflict my idiomatic OCaml because the types were all inferred.

> You are heavily relying on type inference to hide some of that
> overhead, but I don't think you can get away with not giving any
> signature at all in a realistically sized example. After all, the
> challenge was about modularity.

On the contrary, I've been enjoying getting away without type
declarations in
real examples for many years now. :-)
</quote>

The issue here is apparently whether inferred typing is modularity:

http://gbracha.blogspot.com/2011/06/types-are-anti-modular.html?showComment=1312367864429#c8055471612448657189

If I understand correctly, Jon appears to be using compile-time type
inference to avoid writing the types of the reusable interfaces. Thus,
he relies on recompilation of the reusable code in order to enable
reuse with new types.

However, the challenge of the Expression Problem was to reuse code
without recompiling it:

http://copute.com/dev/docs/Copute/ref/Complete%20solutions%20to%20the%20%93Expression%20Problem.htm

Off-the-top-of-my-head thoughts on why this is important (feel free to
correct me please):

1. As the matrix of reuse variants grows more complex, the chances
decrease that they will all compile separately without requiring
incompatible modifications to the reusable code.

2. Binary compatibility (as I read, a major issue being painfully
addressed in Scala libraries now).

3. How does one recompile a public web interface? I.e. Hot-plugging
(hot-swapping) is a reality of networked computing.

Tangentially, I am curious how ML modules impact the above 3 concerns?

======================
Towards comparing OOP (subtyping) and FP (functional composition), I
can add the following.

In terms of solutions to the Expression Problem, I understand that OOP
and FP address orthogonal axis of extension. OOP allows the addition
of subtypes but not new methods without recompilation, and FP allows
the addition of new operations (i.e. methods in OOP) but not new
subtypes without recompilation.

Tangentially note, that Zenger, Odersky claim to enable extension in
both axis in Scala, but I argue that this cannot be accomplished
without violating runtime type-safety (e.g. a 'default' case):

http://copute.com/dev/docs/Copute/ref/Complete%20solutions%20to%20the%20%93Expression%20Problem.htm#8409828

Somewhere I had also analyzed multi-methods and afaics they cannot
solve this dilemma, and the reason is because undecidability is
inherent in open recursion, Russell's Paradox, that Turing-complete is
unbounded recursion, and that knowledge can't exist if it is entirely
enumerated (a static universe violates 2nd law of thermo).

http://stackoverflow.com/questions/7266596/why-avoid-subtyping/8352969#8352969
http://stackoverflow.com/questions/7284/what-is-turing-complete/8283566#8283566
http://copute.com/docs/Event.html#Deterministic_Semantics

In the link above, I made the observation that subtyping is a
bijective contract, and FP is only surjective.

I claim that subtyping is more powerful in because it contracts future
boundaries to the granularity of composition of types, and that this
is dangerous because in general the bijective contract of subtyping is
undecidable (else it is isn't unbounded extensible). Whereas,
functional composition contracts the future granularity of operations,
but one is free to write a new function with finer granularity as the
expensive of reuse of the bloated function.

Then refer back to my point that non-inferred types are important for
reusable APIs and the Expression Problem, so I conclude that the power
of subtyping is a required axis for modularity.

Any thoughts to share?

[Shelby]

I have read the old thread again, and the crux of the debate is
whether there is anything that subtyping can do better than not having
subtyping.

Thus it is also a question about whether there is ever any use case
advantage to fusing functions to a data type.

If a function inputs a collection, whose instances have heterogeneous
data types, the type parameter can be a union of those types. A
function call on this union could in theory be statically type
checked, and dynamically dispatched at runtime to the appropriate
function. Are there any languages which do this? Otherwise the union
can be pattern matched and the appropriate function called. In either
case, new data types can not be added to that input collection by
callers without recompiling the code for the function being called.

Whereas, with virtual inheritance, new data types can be added which
subtype the existing ones without recompiling the pre-existing code.

Thus subtyping is required to solve the Expression Problem along the
axis of adding new data types.

Haskell type classes can do *compile-time* subtyping (but with a
significant limitation, see link in my prior msg), but they can not do
runtime dynamic dispatch, a/k/a virtual inheritance which is runtime
subtyping. These type classes can inherit interfaces (again with a
significant limitation that breaks composition), so there is some
illusion of subtyping that readily breaks down.

Functional programming can add new functions (a/k/a operations) that
operate on existing data types without recompiling code that operates
on the existing data types. Thus FP solves the Expression Problem
along the axis of adding new operations. Programs that have both
subtyping and FP can do both forms of extension.

The next question is whether there is any use case that can not be
done by adding new data types that are subtypes of existing one. I
will leave it as an open question for now. Perhaps someone smarter
than me can provide a unequivocal answer.

[Shelby]

On May 5, 11:23 pm, Shelby <she...@coolpage.com> wrote:
> The next question is whether there is any use case that can not be

Typo: can only be

[John Nilsson]

Another question might be why the distinction between runtime and compiletime is important given JIT-compilation and optimizing virtualmachines?
BR
John

[Shelby]

Thinking of game programming with user scripting extension, assume
there is a function that does some mathematical or physics
optimization, such as finding a least cost path in a dynamic system,
that operates on a collection of objects, who each expose a constant
public interface of *dynamic* attributes, i.e. these attribute methods
input variables for their environment at any given state in the
computation.

These objects will be implemented in different ways with different
sorts of private internal data types and private internal algorithms,
even though the public interface exposed within the function remains
constant. Thus without subtyping, it would be impossible to add new
internal data types and new internal algorithms, without recompiling
the function. The game would not be as extensible for the users.

Afaict, there is no escaping that either dynamic dispatch (or any
theoretical equivalent emulation, such as manually inputting a
parameterized callback) is necessary to be able to change the data
types (note I didn't say interfaces, which remain constant) that a
function operates on. Although it promises defusing the functions from
the data types, I expect with parameterized callbacks it will become
unwieldy to essentially pass around the complex data structures of
vtables manually, along with complex data structures such as nested
heterogeneous collections.

Emulating subtyping is discussed in the following research paper from
1992:

Objects and Subtyping in a Functional Perspective, Odersky

Martin implied the same at some scale of complexity, component
abstraction is required:

On Saturday 02 May 2009 08:32:29 martin odersky wrote:
> I am still not satisfied.
[...]
> At some points you will
> have to introduce component structures

It is claimed that ML functors do not do dynamic dispatch:

Scalable Component Abstractions, Odersky and Zenger

"However, functors still pose severe restrictions when it
comes to structuring components.
Recursive references between separately compiled components are not
allowed and
inheritance with dynamic binding is not available."

[Shelby]

On May 6, 12:13 am, John Nilsson <j...@milsson.nu> wrote:
> Another question might be why the distinction between runtime and
> compiletime is important given JIT-compilation and optimizing
> virtualmachines?
> BR
> John

If I am not mistaken, I don't think recompilation alone helps, either
the code supports the equivalent of virtual dispatch or you will have
to edit the function to add a case and re-compile.

My prior message mentions a research paper on simulated virtual
dispatch without virtual subtyping. I doubt it is as scalable, but I
dunno because I haven't tried it.

As the data structures we operate on because more complex and nested,
then keeping the methods orthogonal from the data they operate on,
would I assume become more unwieldy. I don't understand the benefit of
avoiding that fusing (which is the only benefit I can see, once we
have to simulate virtual dispatch in a language without subtyping)?

Note I am not claiming to be an expert on this topic.

[Jesper Nordenberg]

Shelby skrev 2012-05-05 17:23:
> Haskell type classes can do *compile-time* subtyping (but with a
> significant limitation, see link in my prior msg), but they can not do
> runtime dynamic dispatch, a/k/a virtual inheritance which is runtime
> subtyping.

This pattern can be used to get dynamic dispatch of a type class X:

data AnyX = forall a. X a => AnyX a

instance X AnyX where
...

/Jesper Nordenberg

[Shelby]

On May 6, 2:58 am, Jesper Nordenberg <megagu...@yahoo.com> wrote:
> > Haskell type classes can do *compile-time* subtyping (but with a
> > significant limitation, see link in my prior msg), but they can not do
> > runtime dynamic dispatch, a/k/a virtual inheritance which is runtime
> > subtyping.
>
> This pattern can be used to get dynamic dispatch of a type class X:
>
> data AnyX = forall a. X a => AnyX a
>
> instance X AnyX where

That will work for dynamic dispatch on the methods of the class X but,
in Haskell, pattern matching is always resolved at compile-time.

Here is a more complete example of Haskell's dynamic dispatch:

http://www.haskell.org/haskellwiki/Existential_type#Dynamic_dispatch_mechanism_of_OOP

From the section "Typeclass Solution Can't Virtually Inherit" in a
link from my first post in this thread, wherein I explained that
typeclass inheritance won't scale compositionality (orthogonal
modularity), because of inability to do general multiple inheritance
relationships:

http://copute.com/dev/docs/Copute/ref/Complete%20solutions%20to%20the%20%93Expression%20Problem.htm#8409828

It also links to section 4.4 "Explicit vs. implicit subtyping" of the
following research paper:

Software Extension and Integration with Type Classes, Lammel and
Ostermann

http://homepages.cwi.nl/~ralf/gpce06/paper.pdf#page=8

I quote:

"the default instance would always be applied since the opaque types
cannot possibly participate in any instance selection (because they
are opaque). Clearly, the universal selection of the default instance
defeats the entire purpose of multiple dispatch"

Pattern matching is required to test intersects of different Shape
(e.g. Circle, Rectangle, etc), ecause each distinct pair of Shape
types require a different intersection algorithm. But the pattern
matching is applied at compile-time on the type AnyShape-- a type
which hides the dynamic types. I believe this is because the types in
Haskell are completely erased at compile-time. So I suppose a
different reified implementation of typeclasses could solve this
problem? Yet the significant inheritance compositionality issue would
remain.

I remember another tidbit about a limitation in Haskell's typeclass
parameterization bound w.r.t. to subtyping:

Generics of a Higher Kind, Moors, Piessens, Odersky

http://adriaanm.github.com/files/higher.pdf

"Furthermore, due to subtyping,
Scala supports abstracting over type class contexts, so that
the concept of a bounded monad can be expressed cleanly,
which is not possible in (mainstream extensions of) Haskell"

In any case, isn't this dynamic dispatch in Haskell just a form of
subtyping? The functions of an instance are fused to the opaque
datatype. Have we gained anything compared to OOP subtyping?

[Jesper Nordenberg]

Shelby skrev 2012-05-06 09:26:
> On May 6, 2:58 am, Jesper Nordenberg<megagu...@yahoo.com> wrote:
>>> Haskell type classes can do *compile-time* subtyping (but with a
>>> significant limitation, see link in my prior msg), but they can not do
>>> runtime dynamic dispatch, a/k/a virtual inheritance which is runtime
>>> subtyping.
>>
>> This pattern can be used to get dynamic dispatch of a type class X:
>>
>> data AnyX = forall a. X a => AnyX a
>>
>> instance X AnyX where
>
> That will work for dynamic dispatch on the methods of the class X but,
> in Haskell, pattern matching is always resolved at compile-time.

I fail to see how this construct is related to pattern matching. What it
does is basically attaching the type class dictionary to the "object",
similar to a vtable. You can add new instances of the type class without
modifying existing code, and existing functions working on X will work
unmodified with the new instances.

> In any case, isn't this dynamic dispatch in Haskell just a form of
> subtyping? The functions of an instance are fused to the opaque
> datatype. Have we gained anything compared to OOP subtyping?

No, it's not subtyping. The types for which the instances of the type
class X are defined are not directly related. The type class "binds"
them together.

/Jesper Nordenberg

[John Nilsson]

I was thinking that if there is no compiletime vs runtime dichotomy this would imply that dynamic dispatch is the only option for the language semantics, static dispatch can be an optimization strategy in the VM.

Is there a case for static dispatch besides optimization?

Br
John

[Shelby]

On May 6, 7:48 pm, Jesper Nordenberg <megagu...@yahoo.com> wrote:
> I fail to see how this construct is related to pattern matching.

Since the types are dynamically open, pattern matching needs to be
dynamically resolved, otherwise it is impossible to handle known cases
of types and apply a default action to the unknown (new types) cases.

I agree this an orthogonal issue. I also agree I was incorrect where I
stated Haskell typeclasses don't have dynamic dispatch. But I think I
was correct to say it doesn't have virtual inheritance (which I
conflated with afaict very limited application of dynamic dispatch,
see below).

> > In any case, isn't this dynamic dispatch in Haskell just a form of
> > subtyping? The functions of an instance are fused to the opaque
> > datatype. Have we gained anything compared to OOP subtyping?
>
> No, it's not subtyping. The types for which the instances of the type
> class X are defined are not directly related. The type class "binds"
> them together.

I understand that even though we can't access these opaque data types
when they are hidden behind class AnyShape (your X), you mean for
example the data Circle, Rectangle, etc., can also be used in the
program and they are not subtypes of class AnyShape. The methods are
fused ("bound") to the type class with the instance declaration.

Afaict, we can accomplish this orthogonality in a language with
subtyping by wrapping a class in another class which inherits from
Shape, e.g. class ShapeCircle( x: Circle ) extends AnyShape {...}

In Haskell, where we use AnyShape, we are asking for the benefits of
virtual dispatch, which is also required for subtyping. If we hide
these subtypes from pattern matching to pretend there aren't any, then
we can't do what I stated is impossible above, nor a more important
example below

I am thinking now that the answer is we must have subtyping for open
types, because there appears to another case that Haskell can't do.
Given two functions, one that inputs an AnyShape and another an
AnyShapeCurved, then if the latter calls the former, AnyShapeCurved
must be a subtype of AnyShape. Perhaps there is a way to make this
work in Haskell? Yet even if so, afaict there will be the issue that
inheritance in Haskell has a significant limitation:

http://existentialtype.wordpress.com/2011/04/16/modules-matter-most/

"Also, for example an Ord(ering) of Int 'can only be done one way'. An
OrdDivisible can't be inserted in the inheritance hierarchy between a
supertype Ord and subtype Int (to provide an alternative
implementation of the methods of Ord). Thus an Int can't be an
argument for a function that expects a parameter of type OrdDivisible.
This breaks compositionality, which is afaik one possible reason some
functions in the Haskell Prelude have boilerplate (multiple
definitions) to handle specific types."

Am I missing an alternative perspective?

On May 6, 10:39 pm, John Nilsson <j...@milsson.nu> wrote:
> I was thinking that if there is no compiletime vs runtime dichotomy this
> would imply that dynamic dispatch is the only option for the language
> semantics, static dispatch can be an optimization strategy in the VM.
>
> Is there a case for static dispatch besides optimization?

Are you asking if there is any need for static typing?

[Jesper Nordenberg]

Shelby skrev 2012-05-06 21:40:
> I understand that even though we can't access these opaque data types
> when they are hidden behind class AnyShape (your X), you mean for
> example the data Circle, Rectangle, etc., can also be used in the
> program and they are not subtypes of class AnyShape. The methods are
> fused ("bound") to the type class with the instance declaration.
>
> Afaict, we can accomplish this orthogonality in a language with
> subtyping by wrapping a class in another class which inherits from
> Shape, e.g. class ShapeCircle( x: Circle ) extends AnyShape {...}

Correct.

> I am thinking now that the answer is we must have subtyping for open
> types, because there appears to another case that Haskell can't do.
> Given two functions, one that inputs an AnyShape and another an
> AnyShapeCurved, then if the latter calls the former, AnyShapeCurved
> must be a subtype of AnyShape. Perhaps there is a way to make this
> work in Haskell?

You can define relations between type classes. Here's how you can encode
it (with admittedly quite a bit of boiler plate):

class Shape a where
...

data AnyShape = forall a. Shape a => AnyShape a

instance Shape AnyShape where
...

class Shape a => ShapeCurved a where
...

data AnyShapeCurved = forall a. ShapeCurved a => AnyShapeCurved a

instance Shape AnyShapeCurved where
...

instance ShapeCurved AnyShapeCurved where
...

Now you can do dynamic dispatch and "subtyping" with explicit type
conversion:

fooShape :: [AnyShape] -> Int

fooShapeCurved :: [AnyShapeCurved] -> Int
fooShapeCurved l = fooShape $ map AnyShape l

/Jesper Nordenberg

[Shelby]

On May 7, 6:14 am, Jesper Nordenberg <megagu...@yahoo.com> wrote:
> class Shape a => ShapeCurved a where

Right, but afaik ShapeCurve can't inherit two different supertypes,
e.g. Shape and Curve, c.f. my prior Ord and OrdDivisible comment.

[Jesper Nordenberg]

Shelby skrev 2012-05-07 01:23:
> Right, but afaik ShapeCurve can't inherit two different supertypes,
> e.g. Shape and Curve, c.f. my prior Ord and OrdDivisible comment.

Sure it can:

class (Shape a, Curved a) => ShapeCurved a where

The same "vtable" construct can then be applied for both "supertypes".

/Jesper Nordenberg

[Shelby]

I provided a poor example of what I was trying to illustrate. I mean
where Curved would also inherit from Shape, and Curved would provide
different implementations of the same methods, as compared to Shape. I
understand the names in my example implied that Curved and Shape would
not share any methods.

A better example is:

Foldable
|_ FoldableFwd -|
| |---- DoublyLinkedList
|_ FoldableRev --|---- LinkedList

That can not be achieved in Haskell, where DoublyLinkedList has both a
FoldableFwd and FoldableRev interface, both of which implement the
method `fold` of Foldable in different ways. LinkedList implements
only FoldableRev (or alternatively it could implement both).

Providing two separate methods `foldfwd` and `foldrev` in Foldable,
would not allow us to filter subtypes at *compile-time*, by the
naturally most efficient direction of their fold.

=================
As we discussed earlier about lack of dynamic pattern matching, there
is only one dictionary per function call:

http://www.haskell.org/haskellwiki/OOP_vs_type_classes#There_is_only_one_dictionary_per_function_call

So if we input multiple different opaque subtypes to a function (i.e.
the new types we can due to dynamic dispatch), the compiler must infer
one common supertype and pick that *one* dictionary. That is worse
than I thought. Therefor a function that compares objects in a list is
impossible.

So I am back to asserting that Haskell does not have dynamic dispatch,
and that the dictionary is set by the caller of the function at
*compile-time*. The callee function is accepting a dynamic dictionary,
but only one dictionary per function. The dictionary is not actually
fused together with the instances in the list of instances.

[Jesper Nordenberg]

Shelby skrev 2012-05-07 18:56:
> I provided a poor example of what I was trying to illustrate. I mean
> where Curved would also inherit from Shape, and Curved would provide
> different implementations of the same methods, as compared to Shape. I
> understand the names in my example implied that Curved and Shape would
> not share any methods.

Actually using "ghc -XFlexibleInstances -XUndecidableInstances
-XOverlappingInstances" you can override default methods in "subtypes"
like this:

class Shape a where
foo :: a -> Int
foo a = 1

class Shape a => Curved a where
...

instance Curved a => Shape a where
foo a = 2

instance Shape Circle where
foo a = 3

However, it seems overriding it in multiple abstract subtypes will cause
"overlapping instances" as GHC doesn't seem to think the the "subtype"
is more specific than the "supertype" (but the concrete data type seems
to be).

> So I am back to asserting that Haskell does not have dynamic dispatch,
> and that the dictionary is set by the caller of the function at
> *compile-time*. The callee function is accepting a dynamic dictionary,
> but only one dictionary per function. The dictionary is not actually
> fused together with the instances in the list of instances.

Your reasoning is confusing. Dynamic dispatch is certainly supported
through the construct I've showed you. Now you're talking about
implementation overriding, which is a separate feature.

/Jesper Nordenberg

[Shelby]

On May 8, 1:53 am, Jesper Nordenberg <megagu...@yahoo.com> wrote:
> Your reasoning is confusing. Dynamic dispatch is certainly supported
> through the construct I've showed you.

Correct. I got confused by sections 3.6 and 3.7 of the prior link I
quoted, which (on more careful study) illustrate our prior conclusion.

> Now you're talking about
> implementation overriding, which is a separate feature.

And diamond multiple inheritance of implementation, because
DoublyLinkedList doesn't override the common implementation of
FoldableFwd and Foldable (given forward order the default). For
DoublyLinkedList, only the FoldableRev overrides Foldable's
implementation. For LinkedList, FoldableRev does not override
Foldable's implementation.

[Shelby]

Didn't we conclude that Haskell supports subtyped dynamic dispatch, but not diamond multiple virtual inheritance, thus isn't the follow chosen answer wrong?

http://stackoverflow.com/questions/7234095/why-is-scalas-type-inference-not-as-powerful-as-haskells

[Daniel Spiewak]

No, the chosen answer is correct.  Haskell has bitten the bullet of allowing a considerable degree of undecidability in its type inference.  Some of that is hidden behind flags (such as the ones Jesper used), while others are immediately available to users (e.g. higher-rank types).  Scala could take the same road, but due to the fact that Scala is a primarily object-oriented language, those points of undecidability would be the common, rather than the uncommon case (as they are in Haskell).

Daniel

[Eugene Burmako]

Could you give an example or two of problems that a full-fledged type inference algorithm in Scala would face because of subtyping?

[Daniel Spiewak]

As Scala's subtyping is nominal, this is pretty easy to do:

class Foo {
  def fun: String
}

class Bar {
  def fun: String
}

def baz(x) = x.fun

There's no real way to disambiguate here within Scala's type system.  That right there is enough to kick out Scala, but not quite enough to kick out "subtyping in general".  We can work around the above problem by adding structural types.  So, we infer baz to be of type:

[A]({ def fun: A } => A)

So far so good, but not only do we have subtyping, we actually have objects.  Objects imply certain other properties that must be maintained, most notably open recursion.  (note: this is something Haskell doesn't have to deal with, regardless of how many GHC flags you activate)

def foo(x) = if (x.isEmpty) 0 else foo(x.tail) + 1

Now we're into the land of severe annoyance.  If we try to build a structural type for this, we will fail:

{ def isEmpty: Boolean; def tail: ??? }

So we need recursive types:

µX . { def isEmpty: Boolean; def tail: X }

And our recursive types need to have free polymorphism:

def foldl(xs)(seed)(f) =
  if (xs.isEmpty) seed else foldl(xs.tail)(f(seed, xs.head))(f)

[A, B]((µX . { def isEmpty: Boolean; def head: A; def tail: X }) => B => ((B, A) => B) => B)

…and higher-rank polymorphism:

def foo(xs) = xs.id("bar") + xs.id(42).toString

{ def id[A](a: A): A } => String

Not just rank(1) either, but full-on rank(k) polymorphism:

def foo(xs) = xs.evil(true).id("bar") + xs.evil(true).id(42).toString

{ def evil(b: Boolean): { def id[A](a: A): A } } => String

This is already getting crazy, but the real insanity comes when you try to encode variance:

def foo(x, xs) = x :: xs

[A, B]((A, { def ::(a: A): B }) => B)

That looks fine, but how do you define :: in List?

class List {
  def ::(head) = Cons(head, this)
}

So far so good, but we're really just delegating to Cons.  What does that look like?

Cons: [A]((A, µX . { def head: A; def tail: X }) => (µX . { def head: A; def tail: X }))

That's not strictly correct though, since tail could actually be a different type!  More specifically, tail could be a covariant subtype of our result List.  So, we really need something more like the following (assuming the ability to encode conjunctive type constraints):

Cons: [A, B, C >: A && C >: B]((A, µX . { def head: B; def tail: X }) => (µX . { def head: C; def tail: X }))

At this point, we're starting to get into territory that seems difficult to construct, and we haven't even looked at contravariance!  (which is usually where the really undecidable questions arise)  Even just inferring a recursive type generally requires significant trickery (e.g. presumed fixed points, or special "magic" fold/unfold constructs like tagged ADTs).

To the best of my knowledge, there is currently no proof that Damas-Milner-style type inference is undecidable in the presence of subtyping.  Principle typing almost certainly goes out the window in the presence of variance, and unification-style inference is definitely (read: proven) a no-go in the presence of rank(k) polymorphism (for k > 1).  Since there is no general way (to my knowledge) of eliminating higher-rank polymorphism in the context of an object-oriented language (without crippling parametric polymorphism to the point of uselessness), this alone might be sufficient to put the kibosh on "better" type inference in Scala.

I think the point stands that this is very, very complex stuff, and not something that Scala can just slap onto its existing type system.  (note: I didn't even touch on things like path-dependent types, traits or typeclasses)  Even Haskell hasn't been able to do it successfully – there are a lot of things that its type inference either bails on or (potentially) produces the wrong answer.

Daniel

[John Nilsson]

Is to correct to say that the problems you describe are related to deterministic algorithms? If so, what is the current state of nondeteministic algorithms for this?

BR,
John

[Daniel Spiewak]

Type inference needs to produce a single type T for any term t.  If there is an algorithm that sometimes produces t : T' and at other times produces t : T, then your type inference is undecidable (since no definitive answer can be reached).  One way to solve this is to allow the type inference to produce a set of types for any term.  Thus, t : {T, T'}, but this requires proofs of exhaustiveness to avoid the undecidability problem.  It also has the tendency to make your type system unsound (usually with problems in preservation).

All of the problems I indicated are fundamental, not algorithmic.

Daniel

[Alex Repain]

2012/11/5 John Nilsson <jo...@milsson.nu>

Is to correct to say that the problems you describe are related to deterministic algorithms? If so, what is the current state of nondeteministic algorithms for this?

Valid question, but I don't think it's the way to go. The very purpose of type inference is to get the types RIGHT for you. I'd still prefer a type inference scheme that can not handle hard stuff and let me type it instead, that will silently misunderstand my code in some cases, even sparse...
 

[Rex Kerr]

Do you really want to have a non-deterministic build process (even in the pseudorandom sense)?

You could use heuristics that are not guaranteed to work in all cases, but I don't think you want to try anything nondeterministic.

  --Rex

[John Nilsson]

I was thinking of approaching inference as an optimization problem.

So instead of searching for the type for some term, the problem would in stead be to find the best type for it. Where all options would be valid combinations of fully inferred sub-terms and a set of ambiguity errors reported to the programmer. And best would be measured in some appropriate way like least amount of ambiguity, or mostly definitions requiring annotations or so.

BR,
John

[Oliver Ruebenacker]

     Hello,

  I'm relatively new to Scala and I don't know Haskell, but I'm curious.

On Mon, Nov 5, 2012 at 2:30 PM, Daniel Spiewak <djsp...@gmail.com> wrote:

As Scala's subtyping is nominal, this is pretty easy to do:

class Foo {
  def fun: String
}

class Bar {
  def fun: String
}

def baz(x) = x.fun

There's no real way to disambiguate here within Scala's type system. 

  I'm sorry, I'm lost. I don't see how any language would figure out the type for x, or what this has to do with subtyping (subtypes of Any? But fun is not a member of Any, so what is the significance?).
 

     Take care
     Oliver

[Daniel Spiewak]

That's correct.  No language can figure out an unambiguous nominal type for x.

Daniel

[Alex Repain]

2012/11/5 John Nilsson <jo...@milsson.nu>

I was thinking of approaching inference as an optimization problem.

So instead of searching for the type for some term, the problem would in stead be to find the best type for it. Where all options would be valid combinations of fully inferred sub-terms and a set of ambiguity errors reported to the programmer. And best would be measured in some appropriate way like least amount of ambiguity, or mostly definitions requiring annotations or so.

I understand your point, but I still think it's not worth the challenge.

Let's say you find a good metric to minimize ambiguity and provide the "best" type in any case.
Let's also suppose that your type system stays sound and practicable.

Then as a programmer, you may have meant another type than this "best" type that your compiler finds. In some cases you will notice it through type errors elsewhere in your program, but this can lead to serious skull damage from head-scratching.
 If the compiler may infer a type that I didn't want it to (although it's already the case even with really basic type inference sometimes, see Scala collections for instance), the least I would like is that it triggers a warning when a type has been found but there may be other candidates, those that the compiler judged less relevant.
But then I would like to correct that warning to make sure my program compiles and behaves well, and I'm left with manual type annotation for that...

I'm not saying that your idea is not interesting, that is the kind of research that can make the field progress in some way but, in fine, what you want for your checked program is one only possible type. If you want several, then you want their common super-type, their union, intersection, etc. so long as it is well-defined type, in the type system you are using...

[Daniel Spiewak]

I think another problem you will have is defining "best" in the context of type inference.  Most type inference systems assume "best" is "most general", which seems reasonable but requires principle typing to be decidable.  Some type systems (*cough* Scala) ignore the notion of "best" altogether and go with "whatever comes first to hand" (except in some weird situations in implicit resolution that may or may not be bugs).

So really, who is to say that one type inference result is "better" than another?  Heaven help you if your definition of "better" is different from your users!

Daniel

[John Nilsson]

"So really, who is to say that one type inference result is "better" than another?"

Isn't that part of Paul Philips job description? :P

BR,
John

[Paul Phillips]

On Mon, Nov 5, 2012 at 4:12 PM, John Nilsson <jo...@milsson.nu> wrote:

Isn't that part of Paul Philips job description? :P

It's my job to say it, and it'd nobody's job to listen!

[Shelby]

On Tuesday, November 6, 2012 3:31:11 AM UTC+8, Daniel Spiewak wrote:

At this point, we're starting to get into territory that seems difficult to construct, and we haven't even looked at contravariance!  (which is usually where the really undecidable questions arise)

Isn't this because the contravariant direction exposes the call-by-value (a.k.a. eager, strict) evaluation strategy language to infinite types in the universe (i.e. bottom), whereas covariance only exposes it to infinite possible values, i.e. top:

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/iHpZPvlbFcIJ

In a call-by-need (a.k.a. lazy, total) evaluation strategy language, the covariance would introduce undecidability, because it exposes the infinite types in the universe (i.e. top), whereas contravariance only exposes it to infinite possible values, i.e. bottom (populates every type). This is why Haskell fundamentally isn't doing nominal subtyping, and instead structural typing and some illusions of inheritance that are congruent with the inverted variance induction. Or as Bob Harper said, one evaluation strategy doesn't have logical sums and the other doesn't have logical products.

In the Curry-Howard correspondence, bottom represents a contradiction. I go more into that in the links below.

See also:

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/Bzn6fvU8ndMJ

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/fr9usb8e_UAJ

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/2Uhic20i0BgJ (links to Bob Harper's blog)

If you want to dig deeper:

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/UdrnBQdqCbgJ

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/6NqKvhrM4HgJ

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/5eHmkFPlOrYJ

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/7WXkMPvjLI4J

https://groups.google.com/d/msg/scala-debate/vysv97J0xok/KVEzGI3_a2gJ

[Shelby]

On Tuesday, November 6, 2012 8:59:34 AM UTC+8, Paul Phillips wrote:

It's my job to say it, and it'd nobody's job to listen!

And to be more verbose, you've succinctly (I've noticed you have a habit of being this clever) implied that the inability to agree on what a type means, is the antithesis of compile-time typing. The whole point of typing is to enumerate the invariant semantics. If everyone is disagreeing on the semantics, then they are not invariant any more.

[Daniel Spiewak]

Isn't this because the contravariant direction exposes the call-by-value (a.k.a. eager, strict) evaluation strategy language to infinite types in the universe (i.e. bottom), whereas covariance only exposes it to infinite possible values, i.e. top:

No, it's because the distinction between co- and contravariance often makes it impossible to fix a most general type, since one is effectively comparing types along multiple axes.  In the context of a nominal type system with subtyping and parametric polymorphism, contravariance also yields other, more interestingly undecidable questions.

Daniel

[Shelby]

On Tuesday, November 6, 2012 3:19:53 PM UTC+8, Daniel Spiewak wrote:

Isn't this because the contravariant direction exposes the call-by-value (a.k.a. eager, strict) evaluation strategy language to infinite types in the universe (i.e. bottom), whereas covariance only exposes it to infinite possible values, i.e. top:

No, it's because the distinction between co- and contravariance often makes it impossible to fix a most general type, since one is effectively comparing types along multiple axes.  In the context of a nominal type system with subtyping and parametric polymorphism, contravariance also yields other, more interestingly undecidable questions.

Given this addition insight (thank you), I am now thinking "yes" is the correct answer.

You were writing down increasingly complex pseudo-code (expressing an equation) for the "structural type" (i.e. a wildcard template for all the unknowns and invariants of the inferred type) in the inherently covariant direction of nominal subtyping, then if that inferred type is used in a contravariant position, then the equation for the type must enumerate invariants along both axes of Liskov Substitution Principle (co- and contra-) variance.

I understand the essence of your point is an explosion of variables that describe the most general inferred type, given such a complex model of typing. I believe Scala's typing system has been shown to be Turing complete:

http://stackoverflow.com/questions/4047512/the-type-system-in-scala-is-turing-complete-proof-example-benefits

http://www.scala-lang.org/node/7698

Thus I am contemplating that my prior message was correct at the most reductionist level of conceptualization. The contravariant direction introduces an infinite number of types (in an eager language), and thus explodes the variables for the most general type. We might want to think conceptually that the least, upper bound could be bottom, but you showed that we are not considering a bound of types, but rather a concrete structure for the most general inferred type. Well, as the links in my prior comment pointed out, bottom contains the conjunction of all members of all types in the universe, thus your the structure of your equation will be undecidable due to having infinite variables.

For Haskell which is a lazy language, this structural explosion of inferred members occurs instead in the covariant (i.e. inductive) direction, and this is why Haskell does not have inductive nominal typing. If I understand correctly (not being very experienced in Haskell, but I remember documenting this, see link below) and given this type theory I presented in my prior message, I believe Haskell has coinductive nominal typing, i.e. a new super type can be declared from an existing type. Whereas an eager language can have inductive nominal subtyping, i.e. a new subtype can be declared from an existing type.

Thus we can conclude as you did, that Haskell will not be able to escape this undecidability if it offers open (coinductive) nominal subtyping and both axes of Liskov Substitution Principle variance. Haskell doesn't have true inductive nominal subtyping.

So the global type inference of Haskell (where it works) occurs because subtyping is not used.

Are there valid use cases in Scala, where we might want to allow global type inference, assuming we even could delimit that an expected type is not open for subtyping, e.g. when supporting typeclasses?

In the Expression Problem (see link below), open (inductive) subtyping provisions for adding new subtypes, but not new members a.k.a. operations, without incurring a default case (a run-time typing hole). Functions provisions adding new operations, but not new subtypes. In Haskell, open coinductive subtyping or typeclasses provisions for adding new operations, but not new subtypes. There is no possible unified solution, because it would violate the open (infinite) nature of the universe.

http://copute.com/dev/docs/Copute/ref/Complete%20solutions%20to%20the%20%93Expression%20Problem.htm

So does the question of this thread, "Usefulness of OOP", boil down to what are the use cases that we can not do with typeclasses (adding operations), but we can do with subtyping (adding new subtypes)?

In my first message in this thread, I posited that the usefulness of OOP, is that where ever we want to declare invariants as types, global recompilation of inferred types is not modularity:

https://groups.google.com/d/msg/scala-language/PIhmEeMg-Ms/3AE0udamW5EJ

Thus the usefulness of OOP (subtyping) appears to the "S-modularity" declaration of invariants in the Expression Problem, i.e. it is an inescapable use case:

http://gbracha.blogspot.com/2011/06/types-are-anti-modular.html?showComment=1312367864429#c8055471612448657189

Subtyping is a contract with less compositional degrees-of-freedom than functional interfaces, thus subtyping invariants should be carefully chosen to be minimized and maximally orthogonal:

http://stackoverflow.com/questions/7266596/why-avoid-subtyping/8352969#8352969

Global type inference is an attempt to cheat on this cost-benefit tradeoff, because it fails S-modularity (for example see the binary compatibility issue). Local type inference is the desirable goal.