From: jimka
Subject: type algebra
Date: 
Message-ID: <7a753a9b-5421-453e-93cb-db88955d2f9c@p69g2000hsa.googlegroups.com>
Does the kind of type description language that common list has have a
name.
I.e., the ability to define types in terms of other types such as

type w is a (and x (or y z))

I'd like to find some sources about how to do reasoning in such a
system.
For example. If an object is of type (and (or string number) (or (eql
42) null))
then therefore it is (eql 42).  That is obvious to the human but i'm
interested in how
type inferencers figure it out, but at a conceptual level, and also at
an efficiency level.
Particularly curious to me is how to find contradictory type
definitions efficiently.

Does someone know any references to read about this?

-jim

From: Rainer Joswig
Subject: Re: type algebra
Date: 
Message-ID: <joswig-A8A82E.15163126012008@news-europe.giganews.com>
In article 
<····································@p69g2000hsa.googlegroups.com>,
 jimka <·····@rdrop.com> wrote:

> Does the kind of type description language that common list has have a
> name.
> I.e., the ability to define types in terms of other types such as
> 
> type w is a (and x (or y z))
> 
> I'd like to find some sources about how to do reasoning in such a
> system.
> For example. If an object is of type (and (or string number) (or (eql
> 42) null))
> then therefore it is (eql 42).  That is obvious to the human but i'm
> interested in how
> type inferencers figure it out, but at a conceptual level, and also at
> an efficiency level.
> Particularly curious to me is how to find contradictory type
> definitions efficiently.
> 
> Does someone know any references to read about this?
> 
> -jim

http://www.pipeline.com/~hbaker1/TInference.html

http://citeseer.ist.psu.edu/87589.html
From: John Thingstad
Subject: Re: type algebra
Date: 
Message-ID: <op.t5jqfoiaut4oq5@pandora.alfanett.no>
P� Sat, 26 Jan 2008 15:16:31 +0100, skrev Rainer Joswig <······@lisp.de>:

>
> http://www.pipeline.com/~hbaker1/TInference.html

Nice one! I have never seen a article on type inferencing in Lisp before.
Most enlightening..

--------------
John Thingstad
From: Marco Antoniotti
Subject: Re: type algebra
Date: 
Message-ID: <dcac6db8-e21c-4be7-92d3-5af3470c1ff4@l1g2000hsa.googlegroups.com>
On Jan 26, 5:51 pm, "John Thingstad" <·······@online.no> wrote:
> På Sat, 26 Jan 2008 15:16:31 +0100, skrev Rainer Joswig <······@lisp.de>:
>
>
>
> >http://www.pipeline.com/~hbaker1/TInference.html
>
> Nice one! I have never seen a article on type inferencing in Lisp before.
> Most enlightening..
>

Yes.  But that is not a Hindley-Milner type inferencer.  The reference
article by Ullman is pretty unreadable and the type inferencer is for
a subset of CLtL1.  Still useful though.

Cheers
--
Marco
From: Rayiner Hashem
Subject: Re: type algebra
Date: 
Message-ID: <7410cb40-f411-4d4a-b60e-ff4b0408651f@e6g2000prf.googlegroups.com>
> Does someone know any references to read about this?

Another one of Baker's papers on the subject: http://home.pipeline.com/~hbaker1/Subtypep.ps.gz

It discusses how to figure out subtype relationships between type
specifications.