Re: Type lists and HArray

[Adriaan Moors-2]

[moving to debate from user]

On Fri, Sep 18, 2009 at 2:15 PM, Jesper Nordenberg <megagurka@...> wrote:

Adriaan Moors wrote:

Well, they are intrinsically quite different, as implicit values are decided at compile time, whereas explicit ones are not. Since implicit values "live" in the same period as types, to me it makes sense to involve them (more closely) in the type checking process (note that they have already started to influence type inference to get the builders of the new collection library to work)

I'm still a bit confounded by this (probably due to my limited brain capacity). Take the following example:

class A { type T }
implicit def ia = new A { type T = Int }
class B(implicit val a : A) { type T = a.T }

// This should work I presume
val b1 : B = new B

in principle, yes, but I don't think I call adaptType in all the right places to make this work (haven't tried -- working on my partial type application branch ;-))

  

// Will this give a compiler error (B#T and b2.T are different types)?
val b2 : B = new B(new A { type T = Boolean })

in principle this would be an error (I haven't implemented that, since I hadn't thought of it yet -- good point!)

the RHS has type `B{type T=Boolean}`  (*) (from `B{type T=a.type#T}` where `a.type` gets widened to `A{type T = Boolean}` based on typing the constructor argument `new A { type T = Boolean}`  -- this is the bit that isn't implemented, I guess this is enough to convince me to drop the idea, as it's getting even hairier now)

(*) for simplicity, I glossed over the fact that you can't override the alias type in B, see below

the expected type for `b2` is `B{type T=Int}` (by the logic that is described in my original mail)

 

How do we write the type of b2?

one approach would be to use an "existential value", which is already supported, in combination with allowing to specify constructor arguments in a type (not supported):

  `B(x forSome {val x: A { type T = Boolean }})`, which could be abbreviated to `B(_ : A { type T = Boolean })`

That's pretty unwieldy, though, I admit... :-)

To me, the interesting part of this approach is that it shows how values and types play together. There are two ways to approach this dilemma: keep types and values strictly separated, as in Omega (Tim Sheard), or embrace the dependencies and provide language support for them (Scala, Coq).   In the end, we want to use types to govern the value level, so the latter approach seems more productive.  More concretely, I'm interested in exploring how implicit search and type inference relate, as they both infer entities, albeit at different levels (the former: values, the latter: types, obviously). How can we describe their interaction elegantly? How can our type-level hacking benefit from this interaction?

Thanks for your input!

cheers,

adriaan

[Jesper Nordenberg]

Adriaan Moors wrote:
 > one approach would be to use an "existential value", which is already
 > supported, in combination with allowing to specify constructor arguments
 > in a type (not supported):
 >   `B(x forSome {val x: A { type T = Boolean }})`, which could be
 > abbreviated to `B(_ : A { type T = Boolean })`

That would work, but I don't think it's very intuitive. When you write
"new B(...)" (and B has no type parameters), it's reasonable to expect
it to have type B.

 > To me, the interesting part of this approach is that it shows how values
 > and types play together. There are two ways to approach this dilemma:
 > keep types and values strictly separated, as in Omega (Tim Sheard), or
 > embrace the dependencies and provide language support for them (Scala,
 > Coq).   In the end, we want to use types to govern the value level, so
 > the latter approach seems more productive.

I definitely think it's preferable to only work with types at the type
level. Creating implicit values and functions just to be able to infer a
type seems like a backwards and cumbersome way compared to:

- built-in type expressions: type F[T1, T2] = (T1 <: T2)#IfElse[Int,
Boolean]

- type specialization (a la C++): type F[T] = Boolean; type F[T <: Int]
= Float

- type implicits (and partial application): trait A[T1, T2] {type T =
T2}; implicit type IA = A[Int, Boolean]; type F[implicit T2 <: A[Int,
_]] = T2#T

And there's probably other solutions as well.

 > More concretely, I'm
 > interested in exploring how implicit search and type inference relate,
 > as they both infer entities, albeit at different levels (the former:
 > values, the latter: types, obviously). How can we describe their
 > interaction elegantly? How can our type-level hacking benefit from this
 > interaction?

I think the most important step was taken in 2.8 when type parameters
could be inferred from implicit parameters.

/Jesper Nordenberg

[Colin Bullock]

Fascinating discussion! I wish I could more actively contribute (must say I'm a bit out of my league here), but I was playing around with a type-level implementation of Conway games just the other day and both type equality checks and partial type application would have vastly simplified things.

Keenly following the developments.
- Colin

[Meredith Gregory]

Dear Colin,

Now that sounds interesting! Is your code for type level Conway games web-accessible?

Best wishes,

--greg

On Fri, Sep 18, 2009 at 7:06 AM, Colin Bullock <cmbullock@...> wrote:

Fascinating discussion! I wish I could more actively contribute (must say I'm a bit out of my league here), but I was playing around with a type-level implementation of Conway games just the other day and both type equality checks and partial type application would have vastly simplified things.

Keenly following the developments.
- Colin

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com

[Colin Bullock]

Now that sounds interesting! Is your code for type level Conway games web-accessible?

Not currently. At this point, I have little more down in code than some experimenting around to see how far I could push things.

I'm definitely stretching the limits of my type-fu here (likely why it's so enjoyable), and have run up against a few walls related to cyclic type definitions and "conditional" types for defining ordering over games. I've also yet to find a satisfactory type to represent sets of positions in games so I've resorted to living with the restriction of only dealing with the greatest and least position for left and right respectively (which potentially seems acceptable for numbers, but likely not so for arbitrary games).

If I have some time to put into it, and can satisfy both the compiler and myself, I'd be happy to share what I've come up with on github or somewhere.

- Colin

[John Nilsson]

Given this definition of function I haven't had any problem with partial evaluation:

    trait F {

        type apply[_ <: F] <: F

    }

On Fri, Sep 18, 2009 at 4:06 PM, Colin Bullock <cmbullock@...> wrote:

Fascinating discussion! I wish I could more actively contribute (must say I'm a bit out of my league here), but I was playing around with a type-level implementation of Conway games just the other day and both type equality checks and partial type application would have vastly simplified things.

Keenly following the developments.
- Colin