Showing posts with label abandoned ideas. Show all posts
Showing posts with label abandoned ideas. Show all posts

Tuesday, November 19, 2013

I'm going to have to maybe-kill the cat

In my last post, I discussed problems with the runtime binding of composed objects: if object a has a method foo, and object b also has a method foo, then how does the composed object (a <?> b) behave? In this post, I'd like to explore a separate but related pair of problems: what's the type of a <?> b, both at run-time and compile-time?

(Before you get too far into this post, a disclaimer: this post describes a method of composition and then explains why it doesn't work. If that strikes you as meandering and pointless — if you prefer to read about ideas that might work, rather than those that definitely won't — then you might want to skip this post.)

As before, let me set this up with an example. As an added bonus, you'll get to see the latest revision of Effes' syntax, which is pretty close to complete (now I really mean it!). Since I haven't laid out how composition works, I'll use <?> as a placeholder for "some variant of composition." With that said:

type List[A] = data Node(head:A, tail:List[A]) | Nothing
  put e:A -> List[A] = TODO
  get -> (Maybe[A], List[A]) = TODO

type Box[A] = Maybe[A]:
  put e:A -> Box[A] = TODO
  get -> Maybe[A] = TODO

myList : List[Int] = TODO
myBox : Box[Int] = TODO
myContainer = myList <?> myBox

Here we have two simple types: one representing a linked list, and one representing a box that can contain zero or one items. Their details aren't important. We also have three references: one of type List[A], one of Box[A], and one representing the composition of the first two.

As I discussed in the last post, we have some options with a call like myContainer.put 1. We can take the Schrodinger approach, in which we invoke put on both components of myContainer and then compose those two results; or we can pick one as the "winning" binding and only invoke it.

Let's say we pick the single-bound, "winner" approach; that's the option I was leaning towards in the last post. To make it concrete, let's say that the left-hand side always wins out. That seems reasonable, but what about this situation:

myContainer2 = myContainer.put 123
myVal : Maybe[Int]
myVal = case myContainer2 of
  Box[Int] -> myContainer.get
  _ -> Nothing

In this snippet, we check to see if myContainer is a Box[Int]. It is, so the first pattern will match. This casts myContainer2 to Box[Int] and, within that new context, invokes get. Note that get here has to be bound to the Box version; the List[A] version has a different return type (it returns a pair containing the list's possible head and its tail).

The problem is that myContainer.put was bound to the List[A] method, meaning that the Box component of myContainer never had 123 inserted into it: the value of myVal is Nothing, not 123! This is fully consistent, but it's confusing and violates the principle of least surprise. There has to be a better way!

One possibility is to limit composition such that myContainer2 does not have a runtime type of Box[Int]: the second (catch-all) pattern matches, and the value of myVal is Nothing.

Of course, we always want the runtime type to be a subtype of the compile-time type, so this new approach means that the composed object's compile-time type can't include Box[Int]. We can't generalize that to all compositions, or else the whole idea of composition falls apart and becomes shorthand for the not-very-useful function a <?> b = a.

We can come up with a more precise limit on composition, one that doesn't just throw away the RHS altogether. One approach to compose objects in multiple phases. Here's one such algorithm, in rough terms:

  1. Decompose the RHS object to its constituent objects.
  2. Fold each one of those into the LHS, one at a time. As you fold each object, check to see whether it has any methods that conflict with methods on the composed object; if so, ignore that object (don't fold it in).
  3. Check whether the resulting object has any abstract methods (that weren't given a concrete definition in the composed object). If so, remove the objects that introduced those methods.
These three phases happen separately for both the compile-time type and the runtime type. Here's an example, starting with some types and some objects:

type List[A] =
    ... (put/get, as above)
    size -> Int
type Box[A] = ... (put/get, as above)

type Container:
  isEmpty -> Bool -- abstract method

type Container Box[A]:
  @override isEmpty -> Bool = TODO

intsList : List[Int] = list(1, 2, 3)
intsBox : Box[Int] = box(4)

intsContainer1 = intsBox <?> Container

The List[A] and Box[A] types are as before, except that List[A] now also has a size method.

Let's look at that last line. The LHS is Box[Int] with methods put and get, while the RHS is Container with just one method, isEmpty. There's no overlap in methods, so the composition is straightforward and results in Box[Int] <?> Container for both the compile-time and runtime type.

Okay, so that case works fine. But what about this?

intsContainer2 : Container = intsContainer1
composed2 = intsContainer2 <?> intsList
composedSize = composed2.size

At compile time, that last line looks like Container <?> List[Int], which has no conflicts and thus doesn't remove any types. But the Container component's isEmpty method isn't implemented, so it's removed: the resulting type is List[Int]. We call its size method, which is a pretty reasonable operation to call on a list.

At runtime, the composition looks like (Box[Int] <?> Container) <?> List[Int], and there is a conflict: List[Int]'s methods collide with Box[Int], and we therefore don't fold List[Int] into the composition. That means that the resulting type is just Box[Int] <?> Container — the inverse of the compile-time type! And in particular, there's no size method on that object. Boom.

I've tried a few variants on this sort of decompose-and-recompose theme: decomposing both sides, different handling of abstract methods, etc. Inevitably, the mismatch between runtime and compile-time types always blows up in my face. I don't think there's a way around it.

Unfortunately, I think this leads me to the conclusion that if I'm going to do composition, I have to do composition all the way: Schrodinger-style. This means I'll need to figure out various issues about collapsing the wave form: how does pattern-matching work, and what happens when an object is composed with an object of the same type? For instance, how does "foo" <?> "bar" work?

Tuesday, September 10, 2013

Maybe it's optional?

A lot of functional and functional-inspired languages don't have the concept of null. Instead, they have types called Maybe or Optional — basically a box of 0 or 1 items. Effes is going to take that approach, but I might put a twist on it.

In a nutshell, the idea behind Maybe (I'll settle on Haskell's terminiology) is that there's a Nothing that represents the absense of something, a Just Foo that represents one Foo, and a Maybe Foo type which can be either a Nothing or a Just Foo.

Like other functional languages, Haskell has syntax (called pattern matching) that's kinda-sorta like an instanceof check plus a downcast in Java. Putting it all together looks something like this:

sayHi :: (Show e) => e -> String
sayHi Nothing = "Nothing to say hi to!"
sayHi (Just e) = "Hello, " ++ (show e) ++ "!"

(The (Show e) => syntax just means that e has a show method, which is like Java's toString.) In Effes, a direct translation would be a disjunctive type:

data Nothing
data Just[A] = elem : A
type Maybe[A] = Nothing | Just[A]

sayHi (m:Maybe[A Stringable]) -> String:
  case m of
      Nothing: "Nothing to say hi to!"
      Just e: "Hello, {{e}}!"

Because Effes has a more flexible type system, we can actually get away without the Just part of the Maybe pair. Instead, it looks something like this:

data Nothing
type Maybe[A] = Nothing | A

sayHi (m:Maybe[A Stringable]) -> String:
  case m of
      Nothing: "Nothing to say hi to!"
      e: "Hello, {{e}}!"

There's not a really strong driving force for this, except that it seems a bit cleaner. Instead of a Maybe being "either nothing or a box of one something," it's "either nothing or one thing." Plus it takes advantage of my cool new type system, so that's nice too.

The problem is when the A type is itself a Maybe: Maybe[Maybe[A]]. If we see that it contains a Nothing, does that mean we didn't have anything, or that we had one Nothing? To prevent unreachable code, I'd probably want the type checker to reject this altogether: Maybe[Maybe[String]] would be a type error.

That's not terrible, I guess, but the erroring type could be nestled in some data structure. For instance, if a linked list uses Maybe to signify an end, then LinkedList[Maybe[String]] wouldn't compile — and probably with some unintuitive or frustratingly un-actionable error message.

On balance, I'm leaning towards keeping the Just type. It doesn't add much complexity to the Maybe type, pattern matching keeps the call sites simple, and it eliminates ambiguity.

Monday, July 22, 2013

The path to function resolution is a winding one

Eek, it's been a while since I've written here. I've been putting off a few posts on subtypes and function resolution, because my ideas aren't fully fleshed out. But here's an update, which is mostly some insight into how my thought process is changing.

I originally had a fairly complicated subtyping scheme in mind, because I wanted to support various ways of composing types. A lot of that had to do with the fact that I wanted to be able to write code like:

data Foo(foo : String)
data Bar(bar : String)
data Buzz -- no args

a = Foo("something")
b : Foo = a Bar("another")
c : Foo Buzz = b

The first two assignments are simple, but the third is... weird.
  • a is a Foo
  • a Bar("another") is a Foo Bar, which is a subtype of Foo and can thus be assigned to a Foo-typed reference — in this case, b
  • c : Foo Buz would be neat if it worked, but it'd require jumping through hoops with the subtyping

The reason I want that last line to work is that Buzz may have some neat behavior, including an override of default behavior. Here's a more concrete example:

getNames() : Stack[String] = ...
useNames(names : QuickSize Stack[String]) = ...
useNames( getNames() )

I'm using the definitions of Stack[A] and QuickSize from a while back. Basically, Stack[A] is Sizeable but has O(N) performance for getting a stack's size, while QuickSize can override a Sizeable object's size method to provide O(1) performance.

The problem is that useNames wants that O(1) performance, while getNames doesn't provide it. My original idea was to allow this with some weird, complicated subtyping rules; that's a bad idea, and I'm abandoning it. My next thought was to allow type declarations to implicitly create composite objects, such that this:

c : Foo Bar = Foo(789)

...would be sugar for this:

fTmp : Foo = Foo(789)
bTmp : Bar = Bar()
c : Foo Bar = fTmp bTmp

I think I'm going to abandon this as well, because it's still complicated and doesn't buy much. In fact, given that I want type inference to eliminate most explicit typing, putting so much semantic importance on declared types is actually a pretty counterproductive plan.

So here's my new idea: do nothing!

Here's how it works. Let's say you have getNames() and useNames as above. In that case, the call site just has to add the QuickSize itself:

useNames( QuickSize getNames() )

That's not so hard. It works because QuickSize (getNames()) creates a new object, the composition of the getNames() : Stack[String] and QuickSize. ("Creates" in the conceptual sense; it may be optimized to just a runtime check).

Better yet, the useNames method can get rid of the QuickSize requirement altogether, since it's just an optimization that polymorphism can handle within the method:

useNames(names : Stack[String]) =
  names = QuickSize names
  ...

So, that's where I am right now. This simplifies the subtyping system a lot, though I still have to figure out what to do with generics and covariance (Stack[Int] vs Stack[Num]). And those simplifications in turn simplify function resolution, which is where all this is really headed in the end.

Wednesday, June 19, 2013

Assumption by any other name make an ass of u and mptions

Until now, I've been using the term "assumption" to describe several ideas: interfaces that define behaviors, stateful traits that include implementations, polymorphism and more. Why haven't I used more standard terminology?

Before I get there, a slight diversion. People who work in Java will sometimes ask a question along the lines of, "I want a Map<K,V> where the keys can be of any type, and the values will depend on the key type." For instance, an Integer key would correspond to a value of MyVal<Integer> (for both gets and puts), a String key would correspond to MyVal<String> values, and so on.

The short answer is that you can't define a Map of that sort in Java. The next question is: why not? Isn't that reasonable? And then the real answer comes in: a type system is just a limited theorem checker, and we've known since Turing that we can't come up with an algorithm that will prove everything you want to prove; so we'll always have to draw a type system's line at some place, and this is where we happened to draw it. If Java allowed for those kinds of types, there'd always a slightly more sophisticated use case that you could ask about and wonder why not.

That got me thinking: what if I designed a type system that, though still limited, had an expanded scope? Most type systems define what types a given object can work with (based on its type). What if I designed one that defined what values an object can work with?

Take a quicksort as an example. The "main" recursive step will look something like:

return (quicksort left) + pivot + (quicksort right)

Well, what happens if you get confused (it's late and you're watching TV while coding) and instead flip the two sides:

return (quicksort right) + pivot + (quicksort left)

My idea was that you could define an assumption called Sortable that would describe which values can be, for instance, pushed into a stack:

Sorted Stack[A] requires A :: Ordered st
    push a requires
        size == 0 or
        a >= pop

Now, in order to push into a Sorted Stack[A], firstly the A type has to have an ordering defined (as it does in any statically typed language that would deal with sorted structures), and secondly, you must have proven in the code that the input is >= the stack's head. For instance:

A :: Ordered ->
badPush(s :: Stack[A], v :: A) :: Sorted Stack[A] st
    push s v -- compilation error!

A :: Ordered ->
tryPush(s :: Stack[A], v :: A) :: Sorted Stack[A] st
    if (size s == 0) or (v >= pop s)
        push s v
    else
        s

In the first example, the code couldn't prove that the assumption required of a Sorted Stack[A] is true, so the code failed to compile. In the second example, it could prove it, and everything's fine.

So, that's why I went with the term "assumption." The idea was that the basic components of a program wouldn't be types, but a bunch of assumptions of a more general nature asserted on objects.

The more I played with it, though, the less promising it looked. All but the most trivial examples became too difficult to express, and I kept needing an "escape hatch" for assumptions that would be cumbersome or impossible to prove in the code. The escape hatch would be in the form of telling the compiler, "I know you can't prove this, but trust me on it." Basically, I felt that the escape hatch would be needed so much that it would become the primary form of typing, in which case the language effectively becomes a dynamically typed language that requires static compilation — the worst of both worlds.

So, I've decided to abandon this effort, and instead focus on a more standard definition of types. I'm going to call these traits, though they're different from traits in some other statically compiled languages in that they're attached to individual objects, and not to other types (as they are in Scala, for instance).