🚀 go-pugleaf

In <paula.658247771@shum> paula@SHUM.HUJI.AC.IL (Paula Ross) writes:

>Is there any way in ML that you can create a data type which accepts
>sequences of objects of different types (when the number and types of the
>objects are not known in advance) ?
>i.e. can you create a list type without the restriction that each element of
>the list must be of the same type ?

As far as I know you can only do this using a union type, which means
you have to know what types you will get.  I don't think it can be done
for an arbitary type.


Fraser Wilson			| Of all the knights in Appledore
fraser@bilby.cs.uwa.oz		| The bravest was Sir Thomas Tom
				| He multiplied as far as four
There can be only one!		| And knew what nine was taken from
	- CM			| To make eleven.  He could write
				| A letter to another knight.	- A.A Milne

In article <paula.658247771@shum>, paula@SHUM.HUJI.AC.IL (Paula Ross) writes:
> Is there any way in ML that you can create a data type which accepts
> sequences of objects of different types (when the number and types of the
> objects are not known in advance) ?

When they *are* known in advance, then you can use a datatype as a variant
record (essentially):

   datatype Object = INTEGER of int
                   | STRING of string
                   | ...

If you don't know how many cases you need in advance, then ML is (in
theory) capable of expressing open-ended datatypes that you can add to.
This is currently only available for the built-in type "exn" (the type
of exceptions), so:

   exception A and B of int;
   val list = [A, B 4];
   exception C of string;
   val list = (C "Hello") :: list;


   (A is a constructor of type exn, B has type int -> exn).

But, since you have to introduce a new constructor for each new type you
wish to work with, you have to retain the constructor in order to take
a value apart for that type.

-- 
Nick Rothwell,	Laboratory for Foundations of Computer Science, Edinburgh.
		nick@lfcs.ed.ac.uk    <Atlantic Ocean>!mcsun!ukc!lfcs!nick
~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~ ~~
 "Now remember - and this is most important - you must think in Russian."

>In <paula.658247771@shum> paula@SHUM.HUJI.AC.IL
(Paula Ross) writes:

>>		Is there any way in ML that you can create a data type
>>		which accepts sequences of objects of different types
>>		(when the number and types of the objects are not known
>>		in advance) ? i.e. can you create a list type without
>>		the restriction that each element of the list must be
>>		of the same type ?

In article <fraser.658398987@melomys> fraser@bilby.cs.uwa.oz.au
(Fraser Wilson) writes:
>	As far as I know you can only do this using a union type,
>	which means you have to know what types you will get.
>	I don't think it can be done for an arbitary type.

One might seek to create a union type which
contains within it _all_ possible types
(i.e. as the solution to a recursive type equation).
Unfortunately this violates the requirement
that all type signatures be finite constructions
from the primitive types.

The problem is that typechecking (and type inference)
in the typed lambda calculus is not generally decidable.
To make typechecking decidable, we impose a restriction
on type signatures, such as the one above.
Because such restrictions handcuff the programmer,
one line of reseach seeks to develop restrictions
for decidablilty which maximize polymorphism.

Because compromise between flexibility and safety
will always involve a trade-off, I believe that
untyped functional languages (e.g. those in the LISP/Scheme style)
will never become completely obsolete.

	Frank Silbermann	fs@cs.tulane.edu
	Tulane University	New Orleans, Louisianna  USA

In article <4906@rex.cs.tulane.edu>, fs@caesar.cs.tulane.edu (Frank
Silbermann) writes:
|> ...
|> One might seek to create a union type which
|> contains within it _all_ possible types
|> (i.e. as the solution to a recursive type equation).
|> Unfortunately this violates the requirement
|> that all type signatures be finite constructions
|> from the primitive types.
|> 


Although not in the standard, some versions of ML features the dynamic
type. This type can be used to implement heterogeneous lists of
values whose types are encapsulated as dynamics.

A dynamic value can be seen as a pair (value, type of the value);
ex (in caml V2-6):

#let x = dynamic 3 and f = dynamic (fun x -> x);;
Value x = (dynamic (3 : num)) : dyn
Value f = (dynamic (<fun> : ('a -> 'a))) : dyn

#let list = [f;x];;
Value list = [(dynamic (<fun> : ('a -> 'a))); (dynamic (3 : num))] :
      dyn list

#let classifyDyn = function
#      dynamic (b:bool) -> "bool"
#    | dynamic (n:num) -> "num"
#    | dynamic (l:'a list) -> "list"
#    | dynamic (f:'a ->'a) -> "id"
#    | _ -> "??";;
Value classifyDyn = <fun> : (dyn -> string)

#map classifyDyn list;;
["id"; "num"] : string list

Of course there is one restriction related to the use of the dynamic
constructor: It can't be used in local expressions to encapsulate
a value whose type depends on the environment:

Ex: 

#let g x = dynamic x;;

line 1: cannot generalize type 'a of variable x 
for dynamic expression: dynamic x
1 error in typechecking

Typecheck Failed

- Ascander Suarez
  suarez@decprl.dec.com

In <4906@rex.cs.tulane.edu> fs@caesar.cs.tulane.edu (Frank Silbermann) writes:

>One might seek to create a union type which
>contains within it _all_ possible types
>(i.e. as the solution to a recursive type equation).
>Unfortunately this violates the requirement
>that all type signatures be finite constructions
>from the primitive types.

>The problem is that typechecking (and type inference)
>in the typed lambda calculus is not generally decidable.
>To make typechecking decidable, we impose a restriction
>on type signatures, such as the one above.

Please could you explain this more fully?

I.e. can you show us an example of a recursive type equation
that would cause problems in typechecking, together
with the precise restriction that would cause it
to be disallowed?

fs@caesar.cs.tulane.edu (Frank Silbermann) writes:

  >Because compromise between flexibility and safety
  >will always involve a trade-off, I believe that
  >untyped functional languages (e.g. those in the LISP/Scheme style)
  >will never become completely obsolete.

There is no meaningful expression which has no type. In the 
case of lists consisting of values of different type, functions 
must exist defined over all instances of the "untyped" list in a 
given program to give meaning to the list. Thus the values of the 
list must have some common property (a type). In the very rare case, 
this property is to be just an object; in most other cases, the 
property will be much more specific: e.g. to be a number,
a (graphic) view, etc.

  >Because such restrictions [on signatures] handcuff the programmer,
  >one line of reseach seeks to develop restrictions
  >for decidablilty which maximize polymorphism.

Yes. The pragmatic problem for the design of a strongly-typed language 
maximizing polymorphism (regarding to ML polymorphism) is that its 
much harder for a programmer to keep track of sophisticated decidability 
restrictions then of (in a way) "syntacticly" expressable restrictions 
like non-recursive signatures. And the type-checker must handle 
undecidable problems, e.g. must avoid its own non-termination, still 
giving comfortable error reports.


--
Wolfgang Grieskamp 
wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET