Re: Re: Improve type inference engine

CAHQS_eyh0G9zGnUfCmFba9cWHezKOAr9qVjoP7ntn9FjKSru6Q [at] mail [dot] gmail [dot] com" type="cite">

On 3 January 2012 17:17, HamsterofDeath <h-star [at] gmx [dot] de" rel="nofollow">h-star@gmx.de> wrote:

can you provide some code? i don't know what "type of a call-site" means

Yeah... Let's sketch a pino-encoding of the naturals.
trait Num { ... } trait Zero extends Num { ... } trait Suc[N <: Num] extends Num { ... }
Now, let's parameterise a list over both the element type and the pino-encoding of the length:
trait PList[A, L <: Num] { def head: A; def tail: PList[A, L#pre] } trait PCons[A, L <:L Num] extends PList[A, L] { ... } trait PNil[A] extends PList[A, Zero]
So far so good. How, if we have a length def, we can define it recursively:
def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => 0   case h::t => length(t) }
Right, so if l is of type PList[A, N] then t is of type PList[A, N#pre]. Each recursive call to length is to a list of a different type. If we throw away the type annotation on l, all you can know is that l <: PList[A, _ <: Zero], which includes Any, so now in the wonderful world of dynamic dispatch, we don't even know what is providing length. It could be any def of that name and arity.

Am 03.01.2012 17:02, schrieb Matthew Pocock:

On 3 January 2012 15:49, Dennis Haupt <h-star [at] gmx [dot] de" target="_blank" rel="nofollow">h-star@gmx.de> wrote:

i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

A function could be recursive, but the recursive call-site could be of a different type than the caller. The obvious case would be a list type where the type encodes the length. Each time you recurse on the tail of the list, the function is called with a list of a different type.
Matthew   --
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com gchat: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com msn: matthew_pocock [at] yahoo [dot] co [dot] uk" target="_blank" rel="nofollow">matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com gchat: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com msn: matthew_pocock [at] yahoo [dot] co [dot] uk" target="_blank" rel="nofollow">matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

still:

def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => *type inferred: Int*
  case h::t =>  1 + *recursion detected, ignoring* // i think you forgot the 1+?
}

-> length returns Int
no problem here

Am 03.01.2012 18:55, schrieb Matthew Pocock:

On 3 January 2012 17:17, HamsterofDeath <h-star@gmx.de> wrote:

can you provide some code? i don't know what "type of a call-site" means

Yeah... Let's sketch a pino-encoding of the naturals.
trait Num { ... } trait Zero extends Num { ... } trait Suc[N <: Num] extends Num { ... }
Now, let's parameterise a list over both the element type and the pino-encoding of the length:
trait PList[A, L <: Num] { def head: A; def tail: PList[A, L#pre] } trait PCons[A, L <:L Num] extends PList[A, L] { ... } trait PNil[A] extends PList[A, Zero]
So far so good. How, if we have a length def, we can define it recursively:
def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => 0   case h::t => length(t) }
Right, so if l is of type PList[A, N] then t is of type PList[A, N#pre]. Each recursive call to length is to a list of a different type. If we throw away the type annotation on l, all you can know is that l <: PList[A, _ <: Zero], which includes Any, so now in the wonderful world of dynamic dispatch, we don't even know what is providing length. It could be any def of that name and arity.

Am 03.01.2012 17:02, schrieb Matthew Pocock:

On 3 January 2012 15:49, Dennis Haupt <h-star@gmx.de> wrote:

i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

A function could be recursive, but the recursive call-site could be of a different type than the caller. The obvious case would be a list type where the type encodes the length. Each time you recurse on the tail of the list, the function is called with a list of a different type.
Matthew   --
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

bdSzTA [at] mail [dot] gmail [dot] com" type="cite">

On 3 January 2012 18:10, HamsterofDeath <h-star [at] gmx [dot] de" rel="nofollow">h-star@gmx.de> wrote:

still:

def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => *type inferred: Int*
  case h::t =>  1 + *recursion detected, ignoring* // i think you forgot the 1+?
}

Yeah, oops... 

-> length returns Int
no problem here

This rather assumes that recursion is detected. How can the compiler work out that the 'length' symbol refers to the def currently being defined? There may be some other single-arg length in scope that accepts some type that is more general than PNil.

bdSzTA [at] mail [dot] gmail [dot] com" type="cite">
Matthew  

Am 03.01.2012 18:55, schrieb Matthew Pocock:

On 3 January 2012 17:17, HamsterofDeath <h-star [at] gmx [dot] de" target="_blank" rel="nofollow">h-star@gmx.de> wrote:

can you provide some code? i don't know what "type of a call-site" means

Yeah... Let's sketch a pino-encoding of the naturals.
trait Num { ... } trait Zero extends Num { ... } trait Suc[N <: Num] extends Num { ... }
Now, let's parameterise a list over both the element type and the pino-encoding of the length:
trait PList[A, L <: Num] { def head: A; def tail: PList[A, L#pre] } trait PCons[A, L <:L Num] extends PList[A, L] { ... } trait PNil[A] extends PList[A, Zero]
So far so good. How, if we have a length def, we can define it recursively:
def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => 0   case h::t => length(t) }
Right, so if l is of type PList[A, N] then t is of type PList[A, N#pre]. Each recursive call to length is to a list of a different type. If we throw away the type annotation on l, all you can know is that l <: PList[A, _ <: Zero], which includes Any, so now in the wonderful world of dynamic dispatch, we don't even know what is providing length. It could be any def of that name and arity.

Am 03.01.2012 17:02, schrieb Matthew Pocock:

On 3 January 2012 15:49, Dennis Haupt <h-star [at] gmx [dot] de" target="_blank" rel="nofollow">h-star@gmx.de> wrote:

i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

A function could be recursive, but the recursive call-site could be of a different type than the caller. The obvious case would be a list type where the type encodes the length. Each time you recurse on the tail of the list, the function is called with a list of a different type.
Matthew   --
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com gchat: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com msn: matthew_pocock [at] yahoo [dot] co [dot] uk" target="_blank" rel="nofollow">matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com gchat: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com msn: matthew_pocock [at] yahoo [dot] co [dot] uk" target="_blank" rel="nofollow">matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com gchat: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster@gmail.com msn: matthew_pocock [at] yahoo [dot] co [dot] uk" target="_blank" rel="nofollow">matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

Am 03.01.2012 19:42, schrieb Matthew Pocock:

This rather assumes that recursion is detected. How can the compiler work out that the 'length' symbol refers to the def currently being defined? There may be some other single-arg length in scope that accepts some type that is more general than PNil.

what does the compiler do now? and isn't that a different problem?

Matthew  

Am 03.01.2012 18:55, schrieb Matthew Pocock:

On 3 January 2012 17:17, HamsterofDeath <h-star@gmx.de> wrote:

can you provide some code? i don't know what "type of a call-site" means

Yeah... Let's sketch a pino-encoding of the naturals.
trait Num { ... } trait Zero extends Num { ... } trait Suc[N <: Num] extends Num { ... }
Now, let's parameterise a list over both the element type and the pino-encoding of the length:
trait PList[A, L <: Num] { def head: A; def tail: PList[A, L#pre] } trait PCons[A, L <:L Num] extends PList[A, L] { ... } trait PNil[A] extends PList[A, Zero]
So far so good. How, if we have a length def, we can define it recursively:
def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => 0   case h::t => length(t) }
Right, so if l is of type PList[A, N] then t is of type PList[A, N#pre]. Each recursive call to length is to a list of a different type. If we throw away the type annotation on l, all you can know is that l <: PList[A, _ <: Zero], which includes Any, so now in the wonderful world of dynamic dispatch, we don't even know what is providing length. It could be any def of that name and arity.

Am 03.01.2012 17:02, schrieb Matthew Pocock:

On 3 January 2012 15:49, Dennis Haupt <h-star@gmx.de> wrote:

i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

A function could be recursive, but the recursive call-site could be of a different type than the caller. The obvious case would be a list type where the type encodes the length. Each time you recurse on the tail of the list, the function is called with a list of a different type.
Matthew   --
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

On 3 January 2012 18:50, HamsterofDeath <h-star@gmx.de> wrote:

Am 03.01.2012 19:42, schrieb Matthew Pocock:

This rather assumes that recursion is detected. How can the compiler work out that the 'length' symbol refers to the def currently being defined? There may be some other single-arg length in scope that accepts some type that is more general than PNil.

what does the compiler do now? and isn't that a different problem?

At the moment, the compiler is just fine because it knows the type of l due to the type annotation. The problem happens when we try to infer l without the annotation - it's in this case that length is ambiguous because the type of l is not constrained enough to know that the nested call to length must be a recursive call. If you know the type of l, then you know that the nested call to length is a recursive call.
Matthew

Matthew  

Am 03.01.2012 18:55, schrieb Matthew Pocock:

On 3 January 2012 17:17, HamsterofDeath <h-star@gmx.de> wrote:

can you provide some code? i don't know what "type of a call-site" means

Yeah... Let's sketch a pino-encoding of the naturals.
trait Num { ... } trait Zero extends Num { ... } trait Suc[N <: Num] extends Num { ... }
Now, let's parameterise a list over both the element type and the pino-encoding of the length:
trait PList[A, L <: Num] { def head: A; def tail: PList[A, L#pre] } trait PCons[A, L <:L Num] extends PList[A, L] { ... } trait PNil[A] extends PList[A, Zero]
So far so good. How, if we have a length def, we can define it recursively:
def length[A, N <: Num](l: PList[A, N]) = l match {   case PNil => 0   case h::t => length(t) }
Right, so if l is of type PList[A, N] then t is of type PList[A, N#pre]. Each recursive call to length is to a list of a different type. If we throw away the type annotation on l, all you can know is that l <: PList[A, _ <: Zero], which includes Any, so now in the wonderful world of dynamic dispatch, we don't even know what is providing length. It could be any def of that name and arity.

Am 03.01.2012 17:02, schrieb Matthew Pocock:

On 3 January 2012 15:49, Dennis Haupt <h-star@gmx.de> wrote:

i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

A function could be recursive, but the recursive call-site could be of a different type than the caller. The obvious case would be a list type where the type encodes the length. Each time you recurse on the tail of the list, the function is called with a list of a different type.
Matthew   --
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.com msn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

--
Dr Matthew PocockIntegrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster@gmail.com gchat: turingatemyhamster@gmail.commsn: matthew_pocock@yahoo.co.uk irc.freenode.net: drdozerskype: matthew.pococktel: (0191) 2566550mob: +447535664143