To the list.
-------- Original Message -------- Subject: creating heterogeneous array in the Poly/ML codetree Date: Thu, 10 Mar 2011 16:07:50 -0600 From: Yue Li yli@cse.tamu.edu Organization: CSE Department, Texas A&M To: David Matthews David.Matthews@prolingua.co.uk CC: Gabriel Dos Reis gdr@cs.tamu.edu
Dear David,
Is there any way to create a heterogeneous array in the Poly/ML codetree with known size, but whose elements can be values of any type and I don't necessarily want to use ML-style datatype. For instance, elements in the array can be integer values, or function values or arrays?
Best,
Yue
I'm not sure if this is what you meant, but the type of exceptions is heterogeneous in the sense that all exceptions, no matter what data they hold, have the same type.
This lets you create lists of different kinds of data, where new types of data can be added later. It essentially pushes type-checking, via the exception system, to runtime. You can then package this dynamic access safely in a functor. The idea is used in Isabelle's generic contexts, among other places.
(btw - does anyone know who came with this idea? I think the first time I saw it was in the Isabelle source code 10 years ago or so...)
To quickly get a flavour of the idea here's a little example...
(* exceptions that wrap up some data *) exception StringExpWrapper of string; exception IntExpWrapper of int;
(* generic kind of data: an informal name for the data and the exception that holds the data *) datatype generic_data = GenericData of { kindstr : string, dataexn : exn };
(* helper function to wrap up data in exceptions and give them a kind string *) fun wrap_int i = GenericData { kindstr = "int", dataexn = IntExpWrapper i }; fun wrap_string s = GenericData { kindstr = "string", dataexn = StringExpWrapper s }; fun wrap_generic ex = GenericData { kindstr = "generic", dataexn = ex };
(* To try and pull integer from generic data; will raise the wrapped exception if the kind-string is "int" but the exception is not the IntExpWrapper. *) fun unwrap_int (GenericData { kindstr = "int", dataexn }) = ((raise dataexn) handle IntExpWrapper x => SOME x) | unwrap_int _ = NONE;
(* empty list *) val empty_list = [] : generic_data list; val list1 = [wrap_string "foo", wrap_int 12, wrap_int 3];
(* we can sum the integers in a generic list... *) fun sum_ints l = List.foldr (fn (data,count) => case unwrap_int data of SOME n => count + n | NONE => count) 0 l;
(* a little test to sum of our first generic/heterogeneous list *) val sum1 = sum_ints list1;
(* we can create new kinds of exception for new type of data we want to wrap up and add to our list ... *) exception SomeNewDataExn of int list;
(* now we can extend our old list with elements, even those of the new type *) val list2 = [wrap_int 2, wrap_generic (SomeNewDataExn [1,2])] @ list1;
(* and we can apply the sum function again to this new list... *) val sum2 = sum_ints list2;
best, lucas
On 10/03/2011 22:31, Yue Li wrote:
To the list.
-------- Original Message -------- Subject: creating heterogeneous array in the Poly/ML codetree Date: Thu, 10 Mar 2011 16:07:50 -0600 From: Yue Li yli@cse.tamu.edu Organization: CSE Department, Texas A&M To: David Matthews David.Matthews@prolingua.co.uk CC: Gabriel Dos Reis gdr@cs.tamu.edu
Dear David,
Is there any way to create a heterogeneous array in the Poly/ML codetree with known size, but whose elements can be values of any type and I don't necessarily want to use ML-style datatype. For instance, elements in the array can be integer values, or function values or arrays?
Best,
Yue
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
On 15/03/2011 05:46, Lucas Dixon wrote:
I'm not sure if this is what you meant, but the type of exceptions is heterogeneous in the sense that all exceptions, no matter what data they hold, have the same type.
The query was really about the lower levels where the data structures are untyped but it's worth pointing out the way in which exceptions can be used to get heterogeneous data structures while retaining ML's strong typing.
(btw - does anyone know who came with this idea? I think the first time I saw it was in the Isabelle source code 10 years ago or so...)
I think it was first pointed out to me when I visited AHL in Uxbridge probably in the late 80's. There was a "universal" type in Poly/ML but it involved some unsafe type coercions. Someone there, probably Simon Finn, realised it was possible to get the same effect using exceptions.
Regards, David
On Tue, 15 Mar 2011, Lucas Dixon wrote:
I'm not sure if this is what you meant, but the type of exceptions is heterogeneous in the sense that all exceptions, no matter what data they hold, have the same type.
The idea is used in Isabelle's generic contexts, among other places.
(btw - does anyone know who came with this idea? I think the first time I saw it was in the Isabelle source code 10 years ago or so...)
This probably refers to my version of it, with the functor wrapping that I made around 1999. It elaborates on much older variants that originated in Cambridge or Edinburgh, IIRC.
The shortest current version of the idea is this clone of the universal type from the Poly/ML internal library:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/Pure/ML-Syste...
David Matthews might actually know more about the history. This idea has been used in his code base much longer than in Isabelle.
Makarius
Dear Lucas,
As mentioned by David, I was asking a question regarding lower level code tree data structure.
But still I enjoy reading your interesting code example. I found this approach very useful when I was writing a small interpreter where I need to keep values with different types in an environment table.
Best,
Yue
On 03/15/2011 12:46 AM, Lucas Dixon wrote:
I'm not sure if this is what you meant, but the type of exceptions is heterogeneous in the sense that all exceptions, no matter what data they hold, have the same type.
This lets you create lists of different kinds of data, where new types of data can be added later. It essentially pushes type-checking, via the exception system, to runtime. You can then package this dynamic access safely in a functor. The idea is used in Isabelle's generic contexts, among other places.
(btw - does anyone know who came with this idea? I think the first time I saw it was in the Isabelle source code 10 years ago or so...)
To quickly get a flavour of the idea here's a little example...
(* exceptions that wrap up some data *) exception StringExpWrapper of string; exception IntExpWrapper of int; (* generic kind of data: an informal name for the data and the exception that holds the data *) datatype generic_data = GenericData of { kindstr : string, dataexn : exn }; (* helper function to wrap up data in exceptions and give them a
kind string *) fun wrap_int i = GenericData { kindstr = "int", dataexn = IntExpWrapper i }; fun wrap_string s = GenericData { kindstr = "string", dataexn = StringExpWrapper s }; fun wrap_generic ex = GenericData { kindstr = "generic", dataexn = ex };
(* To try and pull integer from generic data; will raise the wrapped exception if the kind-string is "int" but the exception is not the IntExpWrapper. *) fun unwrap_int (GenericData { kindstr = "int", dataexn }) = ((raise dataexn) handle IntExpWrapper x => SOME x) | unwrap_int _ = NONE; (* empty list *) val empty_list = [] : generic_data list; val list1 = [wrap_string "foo", wrap_int 12, wrap_int 3]; (* we can sum the integers in a generic list... *) fun sum_ints l = List.foldr (fn (data,count) => case unwrap_int data of SOME n => count + n | NONE => count) 0 l; (* a little test to sum of our first generic/heterogeneous list *) val sum1 = sum_ints list1; (* we can create new kinds of exception for new type of data we want to wrap up and add to our list ... *) exception SomeNewDataExn of int list; (* now we can extend our old list with elements, even those of the new type *) val list2 = [wrap_int 2, wrap_generic (SomeNewDataExn [1,2])] @
list1;
(* and we can apply the sum function again to this new list... *) val sum2 = sum_ints list2;
best, lucas
On 10/03/2011 22:31, Yue Li wrote:
To the list.
-------- Original Message -------- Subject: creating heterogeneous array in the Poly/ML codetree Date: Thu, 10 Mar 2011 16:07:50 -0600 From: Yue Li yli@cse.tamu.edu Organization: CSE Department, Texas A&M To: David Matthews David.Matthews@prolingua.co.uk CC: Gabriel Dos Reis gdr@cs.tamu.edu
Dear David,
Is there any way to create a heterogeneous array in the Poly/ML codetree with known size, but whose elements can be values of any type and I don't necessarily want to use ML-style datatype. For instance, elements in the array can be integer values, or function values or arrays?
Best,
Yue
polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml