The Curse of DOT

[Daniel Sobral]

Adriaan, did you made the presentation available somewhere?

--
Daniel C. Sobral

I travel to the future all the time.

[Adriaan Moors]

I hereby have -- please note that these are ideas, not promises

[Miles Sabin]

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaa...@epfl.ch> wrote:
> I hereby have -- please note that these are ideas, not promises

How much beer do I have to feed you to turn them into promises?

Cheers,

Miles

--
Miles Sabin
tel: +44 7813 944 528
gtalk: mi...@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

[Adriaan Moors]

I've tried, but it seems no amount of beer can turn me into Martin.

[√iktor Ҡlang]

On Sun, Jul 17, 2011 at 8:02 PM, Adriaan Moors <adriaa...@epfl.ch> wrote:

I've tried, but it seems no amount of beer can turn me into Martin.

So essentially what could be:
(Adriaan) => (Seq[Beer]) => (Either[Intoxication,Martin])

turned out to be

(Adriaan) => (Seq[Beer]) => (Left[Intoxication, Martin])


I'd like to prove this hypothesis when we meet next time.

Cheers,
√
 

On Sun, Jul 17, 2011 at 12:40 PM, Miles Sabin <mi...@milessabin.com> wrote:

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaa...@epfl.ch> wrote:
> I hereby have -- please note that these are ideas, not promises

How much beer do I have to feed you to turn them into promises?

Cheers,


Miles

--
Miles Sabin
tel: +44 7813 944 528
gtalk: mi...@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

--
Viktor Klang

Akka Tech Lead

Typesafe - Enterprise-Grade Scala from the Experts

Twitter: @viktorklang

[Kevin Wright]

On 17 July 2011 19:02, Adriaan Moors <adriaa...@epfl.ch> wrote:

I've tried, but it seems no amount of beer can turn me into Martin.

Scotch it is then!

When will you next be in the UK?

 

On Sun, Jul 17, 2011 at 12:40 PM, Miles Sabin <mi...@milessabin.com> wrote:

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaa...@epfl.ch> wrote:
> I hereby have -- please note that these are ideas, not promises

How much beer do I have to feed you to turn them into promises?

Cheers,


Miles

--
Miles Sabin
tel: +44 7813 944 528
gtalk: mi...@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

--
Kevin Wright

gtalk / msn : kev.lee...@gmail.com

google+: http://gplus.to/thecoda

mail: kevin....@scalatechnology.com

vibe / skype: kev.lee.wright

quora: http://www.quora.com/Kevin-Wright
twitter: @thecoda

"My point today is that, if we wish to count lines of code, we should not regard them as "lines produced" but as "lines spent": the current conventional wisdom is so foolish as to book that count on the wrong side of the ledger" ~ Dijkstra

[xeno.by]

>>“virtualising” pattern matching (specify its zero-plus monad)
Could you, please, elaborate on this?

>  dot.pdf
> 172KViewDownload

[Andrew]

So, having read through the slides and spent half my time salivating,
and the other half feeling thoroughly confused, can I ask for some
context here?

Is this something that is being actively/officially worked on? (and if
not, why not?!? :-)

Where was this presented?

Ta,
Andrew

[Niels]

Adriaan,

Would you be able to write a blog piece about the ideas you presented?
It looks very interesting, but without some concrete examples and
explanation it looks a bit cryptic.

Niels

[martin odersky]

On Mon, Jul 18, 2011 at 7:16 PM, Niels <nielsh...@gmail.com> wrote:

Adriaan,

Would you be able to write a blog piece about the ideas you presented?
It looks very interesting, but without some concrete examples and
explanation it looks a bit cryptic.

Let us get the paper done first :-) Everything else would be speculation before that is out.

Cheers

 -- Martin

[Niels]

Looking forward reading the paper.

The presentation mentions virtual classes twice. Is that in the
pipeline?

On Jul 18, 7:18 pm, martin odersky <martin.oder...@epfl.ch> wrote:

[Adriaan Moors]

On Mon, Jul 18, 2011 at 9:46 PM, Niels <nielsh...@gmail.com> wrote:

Looking forward reading the paper.

The presentation mentions virtual classes twice. Is that in the
pipeline?

no, i was just discussing the similarities to virtual classes (wrt the challenges to proving properties of the theory, ...)

more generally, these slides were not written to be consumed without me talking over them, sorry!

adriaan

[Adriaan Moors]

On Mon, Jul 18, 2011 at 9:40 AM, xeno.by <xeno.by@gmail.com> wrote:

>>“virtualising” pattern matching (specify its zero-plus monad)
Could you, please, elaborate on this?

this is also very much work in progress -- I'll try to write up some ideas next month

adriaan

[Alex Cruise]

I couldn't find it for myself, so it's worth asking: 

What does DOT stand for? :)

-0xe1a

[martin odersky]

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <al...@cluonflux.com> wrote:

I couldn't find it for myself, so it's worth asking: 

What does DOT stand for? :)

Dependent Object Types.

Cheers
 
 -- Martin

[Alex Repain]

2011/7/19 martin odersky <martin....@epfl.ch>

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <al...@cluonflux.com> wrote:

I couldn't find it for myself, so it's worth asking: 

What does DOT stand for? :)

Dependent Object Types.

Dah, that's a real fiat lux for me ! Looking only at the slides, I almost thought it was some weird name for a Scala branching, or a new compiler plug-in. So that's what it is all about ...

As for the content, it looks really promising (ok, no promise, "proposing" then), and if the intended clean-up in Scala type system is as great a success as the clean-up in Collections was, when Scala 2.8 went out, then I bet I'm going to stick to Scala for some more long and happy years.

Cheers
 
 -- Martin

--
Alex REPAIN
ENSEIRB-MATMECA - student
TECHNICOLOR R&D - intern
BORDEAUX I      - master's student
SCALA           - enthusiast

[Chris Marshall]

So where *do* I go to find out more about Deviant Old Trolls?

[Kevin Wright]

On 20 July 2011 11:23, Chris Marshall <oxbow...@gmail.com> wrote:

So where *do* I go to find out more about Deviant Old Trolls?

It sounds like you haven't had much exposure to IRC recently... The #scala channel is rather good, you know!

[Vlad Patryshev]

Is it so that to have correct union types you already need boolean logic? (As I heard, dependent types do imply boolean logic; not sure if I have the proof around.)

Thanks,
-Vlad

[Vlad Patryshev]

Sorry, and the subsequent question: does not it actually mean we are limiting our abilities as soon as we limit ourselves with boolean logic? Not good for a general-purpose language.

Thanks,
-Vlad

[Randall R Schulz]

On Thursday 21 July 2011, Vlad Patryshev wrote:
> Sorry, and the subsequent question: does not it actually mean we are

> * limiting* our abilities as soon as we limit ourselves with boolean

> logic? Not good for a general-purpose language.

Boolean logic is simple and for deterministic state machines,
ineluctable. I.e., until we're using quantum computers, Boolean logic
is what we're working with.

How do you see it as limiting? Does the excluded middle chafe?

> Thanks,
> -Vlad

Randall Schulz

[Vlad Patryshev]

I mean, Curry-Howard correspondence is between type systems and intuitionistic logic, right? Limiting it to boolean only puts constraints on types, not sure yet how to formulate it properly, but they seem to be too strict.

And, going into philosophy, I disagree with the statement that "boolean logic is what we are working with". Add time-dependency, and there's no boolean logic.

Thanks,
-Vlad

[Meredith Gregory]

Dear Randall,

Hilarious! Actually, Intuitionistic Logic, Intuitionistic Linear Logic or Classical Linear Logic are all wonderful alternatives that are considerably closer to the mark of "what we're working with" when we work with computers. So, Heyting algebras and Quantales to you! ;-)

Best wishes,

--greg

On Fri, Jul 22, 2011 at 7:35 PM, Randall R Schulz <rsc...@sonic.net> wrote:

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SW

Seattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

[Ruslan Shevchenko]

Аctually, 2-value logic is still enough, because for any N-value
logic we can build 2-value view
with normal (false, true) values and extra predicate symbols
(This morphism will defined for each 'n-logic' value 'x', predicate
symbol(f is 'value-x'))

I.e. boolean algebra is a minimal mental structure, where we can
formalize difference between some
two things.

[Vlad Patryshev]

When you say "enough", I wonder, enough for what? Why is "difference  between two things" so essential? Yes, the minimal logic for two logical values is a two-valued logic. But not every logic consists of values.

As to essential non-booleanness, here's an example: functions from arbitrary sets to finite sets: they do form a topos, but there's no underlying boolean topos.

Anyway, it would be curious to see how you model any intutionist logic with boolean, using predicates; any references?

Thanks,
-Vlad

2011/7/22 Ruslan Shevchenko <ruslan.s....@gmail.com>

[Ruslan Shevchenko]

I see, you understand my words 'can be view as' as ' exists, mapping,
where values of non-classic logic
are mapped to boolean values'. This misunderstanding сan be causes
by my negligence in the terminology, so sorry about this,

I mean: exists mapping, where formulas of non-classic logic mapped to
formulas in classic logic'.
Simplest case is derivalbility: G |- v-<n>(x) when value(x) is <n>

For intutionist logic, formulas, appropriative for logical values will be:
x|- A, |- ~~A, X|- ~~~~A from one side and x|- ~A, x|- ~~~A .....
from other ;)

Links -- I will think about this during next week and may be will
write a post in blog for you when have time
(as I understand, this discussion is far from scala-language; )

2011/7/23 Vlad Patryshev <vpatr...@gmail.com>:

[Vlad Patryshev]

Okay, I kind of guess what you might mean. You can apply this solution to the logic of the topos I mentioned above.

Thanks,
-Vlad

2011/7/23 Ruslan Shevchenko <ruslan.s....@gmail.com>