The Curse of DOT

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

On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral <dcsobral@gmail.com> wrote:

Adriaan, did you made the presentation available somewhere?

--
Daniel C. Sobral

I travel to the future all the time.

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors 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

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

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

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaan.moors@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: miles@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

On Sun, Jul 17, 2011 at 8:02 PM, Adriaan Moors <adriaan.moors@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 <miles@milessabin.com> wrote:

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaan.moors@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: miles@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

--
Viktor Klang

Akka Tech LeadTypesafe - Enterprise-Grade Scala from the Experts

Twitter: @viktorklang

On 17 July 2011 19:02, Adriaan Moors <adriaan.moors@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 <miles@milessabin.com> wrote:

On Sun, Jul 17, 2011 at 3:33 PM, Adriaan Moors <adriaan.moors@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: miles@milessabin.com
skype: milessabin
http://www.chuusai.com/
http://twitter.com/milessabin

--
Kevin Wright

gtalk / msn : kev.lee.wright@gmail.comgoogle+: http://gplus.to/thecoda
kev.lee.wright@gmail.commail: kevin.wright@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

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

On Jul 17, 5:33 pm, Adriaan Moors wrote:
> I hereby have -- please note that these are ideas, not promises
>
>
>
> On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral wrote:
> > Adriaan, did you made the presentation available somewhere?
>
> > --
> > Daniel C. Sobral
>
> > I travel to the future all the time.
>
>
>
>  dot.pdf
> 172KViewDownload

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

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

On Jul 18, 9:41 am, Andrew wrote:
> 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

On Mon, Jul 18, 2011 at 7:16 PM, Niels <nielshoogev1@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

Looking forward reading the paper.

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

On Jul 18, 7:18 pm, martin odersky wrote:
> On Mon, Jul 18, 2011 at 7:16 PM, Niels 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

On Mon, Jul 18, 2011 at 9:46 PM, Niels <nielshoogev1@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

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

I couldn't find it for myself, so it's worth asking: 
What does DOT stand for? :)
-0xe1a

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex@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

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

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex@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

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

On Tue, Jul 19, 2011 at 9:26 PM, martin odersky <martin.odersky@epfl.ch> wrote:

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex@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

On 20 July 2011 11:23, Chris Marshall <oxbowlakes@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!  

On Tue, Jul 19, 2011 at 9:26 PM, martin odersky <martin.odersky@epfl.ch> wrote:

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex@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

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


On Sun, Jul 17, 2011 at 7:33 AM, Adriaan Moors <adriaan.moors@epfl.ch> wrote:

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

On Sat, Jul 16, 2011 at 10:12 AM, Daniel Sobral <dcsobral@gmail.com> wrote:

Adriaan, did you made the presentation available somewhere?

--
Daniel C. Sobral

I travel to the future all the time.

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


On Wed, Jul 20, 2011 at 3:30 AM, Kevin Wright <kev.lee.wright@gmail.com> wrote:

On 20 July 2011 11:23, Chris Marshall <oxbowlakes@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!  

On Tue, Jul 19, 2011 at 9:26 PM, martin odersky <martin.odersky@epfl.ch> wrote:

On Tue, Jul 19, 2011 at 8:05 PM, Alex Cruise <alex@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

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

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


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

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

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 <rschulz@sonic.net> wrote:

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

--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SWSeattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

А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.

On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
wrote:
> 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 wrote:
>>
>> 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
>
>
>
> --
> L.G. Meredith
> Managing Partner
> Biosimilarity LLC
> 7329 39th Ave SW
> Seattle, WA 98136
>
> +1 206.650.3740
>
> http://biosimilarity.blogspot.com
>

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.shevchenko@gmail.com>

 А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.

On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
<lgreg.meredith@gmail.com> wrote:
> 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 <rschulz@sonic.net> wrote:
>>
>> 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
>
>
>
> --
> L.G. Meredith
> Managing Partner
> Biosimilarity LLC
> 7329 39th Ave SW
> Seattle, WA 98136
>
> +1 206.650.3740
>
> http://biosimilarity.blogspot.com
>

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-(x) when value(x) is

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 :
> 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
>>
>>  А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.
>>
>> On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
>> wrote:
>> > 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
>> > wrote:
>> >>
>> >> 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
>> >
>> >
>> >
>> > --
>> > L.G. Meredith
>> > Managing Partner
>> > Biosimilarity LLC
>> > 7329 39th Ave SW
>> > Seattle, WA 98136
>> >
>> > +1 206.650.3740
>> >
>> > http://biosimilarity.blogspot.com
>> >
>
>

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.shevchenko@gmail.com>

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 <vpatryshev@gmail.com>:
> 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.shevchenko@gmail.com>
>>
>>  А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.
>>
>> On Sat, Jul 23, 2011 at 8:18 AM, Meredith Gregory
>> <lgreg.meredith@gmail.com> wrote:
>> > 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 <rschulz@sonic.net>
>> > wrote:
>> >>
>> >> 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
>> >
>> >
>> >
>> > --
>> > L.G. Meredith
>> > Managing Partner
>> > Biosimilarity LLC
>> > 7329 39th Ave SW
>> > Seattle, WA 98136
>> >
>> > +1 206.650.3740
>> >
>> > http://biosimilarity.blogspot.com
>> >
>
>