Lambda the Ultimate

Thank you, I'll take a look at those suggestions.

I'd not thought about the security implications before – Good area for consideration, although I think it would be something that could be understood better once it was available.

I think the library or language thing is a greyer devision, but there's no reason why what I've got in mind wouldn't work as a library, at least for a lisp like language, where a library can have access to program code. There are advantages to this being fairly baked in though, so that ubiquitous access makes it the natural way to build a system. I think it's also likely to benefit from the compiler or interpreter having a very close understanding of it for optimisation.

On your points:

a) There can be issues of ambiguity with the most specific implementation, although my current thinking is that these can be flagged during a compilation phase fairly easily.

The specific example you give is a great clarification.I don't believe to be a significant problem because it's a case of cowboy.draw() and artist.draw(). I saw this mentioned on LtU yesterday and I thought it was a brilliant description for the issue :-) In this case specifically, the rounded rectangle would have a "corner-radius" member, not a "radius" member.

More generally, namespaces would almost certainly be necessary in any kind of reasonably large system to ensure that syntactically equal, but semantically divergent names can't be confused. Or equally, to ensure that semantically equal but syntactically different names can be seen as equivalent.

b) What I've got in mind allows for the compiler to determine the possibility of an ambiguous call being made, but it would know nothing of the certainty that it will be. It also doesn't provide compile time checking that a method will be called with completely incompatible arguments. I have some optimism that this might be possible, but I've not really begun to think about it yet.

For me, static type checking is not a great requirement. IMHO few of the bugs I make in programs would be avoided by static type checking. Those I do make manifest very rapidly and I'd much rather see energy invested in better live coding and rich debugging / REPLs.

I find static type checking much more compelling when it is providing an element of dispatch, such as with Haskel pattern deconstruction. I've a suspicion there are other powerful advantages to static typing facilitating abstraction, and that the whole static error checking thing is a bit of a distraction between dynamic and static proponents. Er, but I'm getting off topic :-)

c) I'm happy for a program to just halt at this point, or throw an exception.

Since you're thinking of static typing, this is how I imagine writing the static types for your example while forbidding ambiguous usage:

width : HasWidth a -> a
height : HasHeight a -> a

area : ((HasWidth Num AND HasHeight Num) -> Num)
  XOR ({radius: Num} -> Num)

where
HasWidth a = {width: a} XOR {square_size: a}
HasHeight a = {height: a} XOR {square_size: a}

Could someone who knows about union and intersection types comment on this? I just tried looking up "symmetric difference type" for XOR here, but I didn't find anything.

Thanks, I'll look that up.

The approach you're suggesting is doable, but easily leads to problems: (a) selection of implementations can be non-deterministic and difficult to guess (e.g. try area on a 'rounded-rectangle' that has both height, width, and radius). (b) it can be difficult to resolve without executing, (c) if executing, may need some sort of rollback in case of side-effects on a failing path.

A while back I put together function calls and backtracking semantics for a very similar effect, and it had these drawbacks. Fortunately, it looks like that's not what the OP has in mind. :)

I can better understand this now, I think:

One implementation approach would be to try to run all available methods and pick the best one at the end. An advantage if this is it's probably achievable with a library in most languages. It avoids the need to be able to parse implementations to understand their signatures.

I think the issues with it are too great though. However, it does suggest a middle ground that would allow testing – implement as a library without source access and have the developer specify an implementations signature by hand.

Or I could just get on with learning macros in Scheme or Scala properly.

I've taken a look at CES & BOT, thank you. It's nice to catch up with Light Table again after seeing the KickStarter.

BOT's tags definitely have a flavour of what I'm after (Although I want to recursively chain on methods by virtue of actual arguments supporting the interface that the methods need – I'm not sure Chris Granger's tags do that, but they surely could). The specification of components that data has, and the implementation of associated functionality separately also seems related.

Thanks for the pointers.

Nimrod uses relatively classic multi-parameter dispatch, except it dispatches not only on types but on so-called "type classes", which are names for types predicate/constraints defined by a runtime contract that is dynamically run.

User-defined Type Classes (Nimrod manual)

type
  Container[T] = generic c
    c.len is ordinal
    items(c) is iterator
    for value in c:
      value is T

A type `Foo` satisfies `Container[Foo]` whenever, when `c` is replaced by a dummy value of type `Foo`, the code block belows compiles and returns `true`. This means that the "is" checks (dynamic satisfaction of types or type-class constraint) must all succeed, the method lookups in the code block must succeed for `Foo`, etc.

Note that no effort is made to recover from potential side-effects (except compilation failure) that would occur during such an execution -- or to even specify what would happen in such a situation.

Dylan, like Common Lisp, is nominally rather than structurally typed.

Thank you for the thought!

I was familiar with DLV. "DLV is a deductive database system, based on disjunctive logic programming, which offers front-ends to several advanced KR formalisms." (what ever that means), although it's been a few years.

When I was using DLV I played about with some of the earlier ideas I had for this and they seemed to be well described with it.

:-) Do you pop up in other discussions of typing systems to mention that their approach is trivially specified by first order logic ;-)

No, that's unfair because going back to the DLV thing, I think it affected my thinking quite a lot (relational DBs too), so it would make sense if what I envisage has a lot of cross over. Definitely the image I have methods chaining primitive structural types outwards so that they pick up a kind of cloud of methods about them, is very similar to Prolog's unification (Is that the right term? – pun happenstantial)

I think Prolog as you show here would also get problems when an implementation is a subtype specialisation of another implementation because Prolog would instantiate atoms for both the super type and the subtype's implementations. I imagine fairly simple extensions address that though. They would need to explicitly tracking how specifically a given implementation's use of formal parameters matches the actual arguments passed.

Probably the plan I have for picking up ambiguity and the option for adding implementations to resolve it would work okay in Prolog.

I'm pretty sure I know how multiple dispatch can work, and possibly also, how dynamic variable bindings (as opposed to lexical ones) can fit in to the dispatch mechanism. I wonder if they might get a bit unwieldy with Prolog… but I don't really know.

Anyway, yes, thank you for reacquainting me with a forgotten influence! That's quite encouraging, in fact.

I'll take a look at Pure, thanks.

Could you talk about this a little further? I presume you were also (implicitly?) typing the fields of the structures, rather than fields being dynamically typed?

I had explicitly, statically typed fields. It's hard to make a concrete example, but the core problem was that the type checker wanted to determine if B was a subtype of A.

So it checked if B satisfied A's structure. But A requires some function 'foo' -> A -> void, which B does not have. But there's a free function 'foo' -> C -> void. So we check to see if B satisfies C's structure, which would let it satisfy A's structure. And then it cascades from there, often into cycles/loops.

Is this an implementation issue? What happens if you memoise the types you have proved already and just use the previous answer when it gets asked for again in the loop?

Structural subtyping should just be unification (ie pattern matching on types) and this is decidable providing you stick to first order types.

I'm going to guess that if it can happen with types referring to each other, it can probably be arranged to happen with an infinite sequence of different types, so that memoizing wouldn't help. (As you say, seems unlikely to be first-order.)

(My own experience with nontermination and types was when I was, typically for me, trying to make types first-class objects in an interpreter with no phase distinction. A type had two methods, one to determine whether a given object was an ancestor, one to determine whether a given object was a member. I liked being honest about the computational nature of the type system; but the opportunites for bizarre behavior, both unintentional and deliberate, were appalling, and I eventually abandoned the project out of sheer fright.

I could memoize the types once proven, but they've not been proven at that point. I do that for other things (inheritance cycles for example), but it ran into issues for this particular problem.

It very definitely could be an implementation issue, or something I'm blanking on due to my informal training. Real life showed up, so I haven't had much time to play around with the hobby project recently.

Something seems odd there. In structural sub-typing I thought that whether a type 'a' is a subtype of 'b' should depend only on the structures of 'a' and 'b'. Should a free function be considered part of the structure of 'a' or 'b'?

I would like it to be. Consider basic things like string + int (for append this number to the string). Without some semblance of free functions as part of the subtyping you can't be guaranteed that this operation is available for more general types.

Normally this would only be an annoyance (see Java and C# generics), but Tangent's phrase concept utilizes this sort of thing quite a bit - perhaps to its detriment.