Question about the type system
Ben Chambers
Milner since I'm working on writing a type checker/infererer for my
Cat in Scheme implementation, and I was wondering why the list type
isn't parameterized. Specifically, why isn't the type of (1 2 3) int
list? If you wanted a variant list (1 2 [3]), you could get this by
simply having a var list (where var is the variant type).
I'm sure this won't be the last question, but I'll try to keep it to a
minimum.
Thanks,
Ben Chambers
Christopher Diggins
Feel free to ask as many questions as you want. People are signed up
on this list, because they are interested in this sort of thing (or
they think that their pet is trying to communicate with them).
The answer is because I haven't gotten to it yet, and I can't decide
on the syntax. I am thinking that maybe t* is the way to go for a list
of t's?
Any thoughts?
- Christopher
Ben Chambers
is nice because it is very concise, and doesn't explode when you want
somethnig like [int * [int]]. Standard ML and OCaml use "t list",
which is kind of annoying because it leads to a bunch of parentheses
problems -- for instance "(int * (int list)) list". Most languages
for writing grammars use t* to mean 0 or more t so I could see that
making sense as well. I think it would run into a problem similar to
the "t list" however when you started to nest them. Square brackets
are an option for Cat, but not really feasible in Scheme since [] and
() are the same, so I would have to end up using (list t). I don't
think that would fit horribly well with your stuff, but I think it
offers some advantages (in my mind) over "t list", specifically (list
int (list int)) is slightly cleaner (and we've added an assumed *).
I'd say it's whatever you feel meshes the best with the syntax of your
language. I think the "t list" will probably fit in with what you
have (since it almost seems to be what you've been doing already). In
the Scheme version I'll probably use "(list t)" once you add
polymorphic list typing.
Another question comes up of whether or not you want heterogeneous
lists to be typed. Specifically, is "(1 2 true)" a variant list or
something else? This should probably be either a variant list or a
tuple -- I don't want to see some horrible syntax for specifying
heterogeneous lists with restrictions...
Tuples would also prove some extra things safe for instance, right now
if you had a list of pairs to add together you would probably do
something like:
1 2 pair uncons [uncons] dip add_int popd
to add the two elements of the pair together. But there is no way to
prove that the two uncons are actually safe without knowing the length
of the list.
But I think that that tuples will probably take a bit longer to
implement (since they'd also require some new primitives), so I'm more
concerned with getting *something* working... to that end I think I'll
start with assuming "t list" (or something equivalent) is part of the
Cat type system and use the S-Expression equivalent in the Scheme
interpreter.
-- Ben Chambers
On Oct 5, 2:39 am, "Christopher Diggins" <cdigg...@gmail.com> wrote:
> Hi Ben,
>
> Feel free to ask as many questions as you want. People are signed up
> on this list, because they are interested in this sort of thing (or
> they think that their pet is trying to communicate with them).
>
> The answer is because I haven't gotten to it yet, and I can't decide
> on the syntax. I am thinking that maybe t* is the way to go for a list
> of t's?
>
> Any thoughts?
>
> - Christopher
>
Ben Chambers
original question regarding t*. I think it would be ok although it
has the same problems as list, but since I suggested using list
anyways. Just keep in mind that eventually you'll see things like:
(a, b) or (a * b) as tuples
Then you'll have:
(a, b)* the list of tuples of a and b
(a, a*)* the list of tuples of a and a lists
or:
(a * b)* the list of tuples of a and b
(a * a*)* the list of tuples of a and a lists
I think that using * for both lists and tuples is clearly a bad idea.
MLs version of teh above would look like:
(a * b) list
(a * b list) list
Which isn't too bad, and haskell's would be:
[(a, b)]
[(a, [b])]
As far as which one you like the best, it's still up to you. The star
should work, but it would pretty much force you to use something other
than * for tuples.
-- Ben Chambers
On Oct 5, 2:39 am, "Christopher Diggins" <cdigg...@gmail.com> wrote:
> Hi Ben,
>
> Feel free to ask as many questions as you want. People are signed up
> on this list, because they are interested in this sort of thing (or
> they think that their pet is trying to communicate with them).
>
> The answer is because I haven't gotten to it yet, and I can't decide
> on the syntax. I am thinking that maybe t* is the way to go for a list
> of t's?
>
> Any thoughts?
>
> - Christopher
>
Christopher Diggins
I appreciate you sharing your thoughts on the issue. They have given
me some ideas.
I am now currently leaning towards a syntax like: "list[a]", "tuple[a,
b]", "pair[a]". What I like about this is that it minimizes the number
of new symbols, it nests well, and it communicates the notion that
such things can be viewed as functions on types.
Any more thoughts on the subject?
- Christopher
Ben Chambers
a]"? I just sat in on an interesting talk discussing type systems for
extensible records, which may be useful to Cat. I'll look into it
once I have a bit more of the type system written. Bascially it
allows you to have an empty record, and then add fields to it -- but
in such a way that adding a field returns a new type. You can also
remove a field, and compose two records. What is interesting is that
everything is well typed, so that you can say:
get_name :: { name : 'a, ...} -> 'a
And get_name will throw an error if it is ever called on a record that
doesn't have a name field. It seems like something like this could be
useful because we could add:
empty_record :: 'S -> 'S {}
add_field :: 'S {...} 'a field -> 'S {field:'a, ...}
get_field :: 'S {field:'a, ...} field -> 'S 'a
remove_field :: 'S {field : 'a, ... } field -> 'S {...}
concat_record :: ???
Like I said, I'm hoping to look into this more after I get done with
the basic type system.
-- Ben Chambers
On Oct 5, 12:18 pm, "Christopher Diggins" <cdigg...@gmail.com> wrote:
> Hi Ben,
>
> I appreciate you sharing your thoughts on the issue. They have given
> me some ideas.
>
> I am now currently leaning towards a syntax like: "list[a]", "tuple[a,
> b]", "pair[a]". What I like about this is that it minimizes the number
> of new symbols, it nests well, and it communicates the notion that
> such things can be viewed as functions on types.
>
> Any more thoughts on the subject?
>
> - Christopher
>
Ben Chambers
lattice? Specifically, if I were to ask an integer for it's type,
would it respond integer? The reason I ask is because this would
influence the shape of the type lattice:
If integers and string respond to the same messages as variant, but
the answers are known statically, then you could have:
var
/ \
int string
\ /
bottom
(there are other types, but I'm not bothering to show them).
But, if primitives like type_of truly only apply to variants, then you
would need:
top
/ | \
int var string
\ | /
bottom
I'm thinking from what I can see of the primitives it seems like it's
the first one. That if I did
5 type_of I would get back integer
Is this correct?
Christopher Diggins
> lattice? Specifically, if I were to ask an integer for it's type,
> would it respond integer? The reason I ask is because this would
> influence the shape of the type lattice:
>
> If integers and string respond to the same messages as variant, but
> the answers are known statically, then you could have:
> var
> / \
> int string
> \ /
> bottom
>
> (there are other types, but I'm not bothering to show them).
>
> But, if primitives like type_of truly only apply to variants, then you
> would need:
> top
> / | \
> int var string
> \ | /
> bottom
>
> I'm thinking from what I can see of the primitives it seems like it's
> the first one. That if I did
> 5 type_of I would get back integer
>
> Is this correct?
Well I'll be honest, I hadn't given the matter that much thought. I am
inclined towards the first version, but I'll have to give it some
careful deliberation.
Cheers,
Christopher
Christopher Diggins
> a]"?
It should be equivalent. Just like two functions can return the same result.
> I just sat in on an interesting talk discussing type systems for
> extensible records, which may be useful to Cat. I'll look into it
> once I have a bit more of the type system written. Bascially it
> allows you to have an empty record, and then add fields to it -- but
> in such a way that adding a field returns a new type.
Sounds like my top-secret undocumented object system. :-)
Which incidentally is in the source code if you feel like browsing C#
source code. A breeze when you use Visual C# express.
> You can also
> remove a field,
That one strikes me a bit odd. I see how one can do it, but I don't
see a particular motivation (yet).
> and compose two records.
Yeah that is a very nice feature.
> What is interesting is that
> everything is well typed, so that you can say:
>
> get_name :: { name : 'a, ...} -> 'a
>
> And get_name will throw an error if it is ever called on a record that
> doesn't have a name field. It seems like something like this could be
> useful because we could add:
>
> empty_record :: 'S -> 'S {}
> add_field :: 'S {...} 'a field -> 'S {field:'a, ...}
> get_field :: 'S {field:'a, ...} field -> 'S 'a
> remove_field :: 'S {field : 'a, ... } field -> 'S {...}
> concat_record :: ???
>
> Like I said, I'm hoping to look into this more after I get done with
> the basic type system.
So Cat already has something similar (but more limited) which I
haven't yet documented. My approach in the is to use "meta-values" as
accessesors. A meta-value is a constant value which is known directly
to the type system and that does not change. Objects provide
"set_field" and "def_field" functions (or something like that, I don't
have the source code in front of me and I implemented it a while ago)
... which have a type signature that requires meta-strings. These
functions return new objects, so are also pure functional. That's it
in a nutshell.
Cheers,
Christopher
Ben Chambers
like:
compare_ages (x, y) = x.age < y.age
(in a language where < applies to multiple things) the inferred type
is {age: 'a, ...} * {age: 'a, ...} -> bool
The removal operator is in some ways a technique for hiding. If I
have a record with a mutable cell, a field containing a function to
set it, a field containing a function to increment it, and a field to
access it, I can restrict you're ability to do things by only giving
you access to the record minus the set function and the mutable cell.
I'm not 100% sure if this would actually work -- like I said, I plan
on reading the papers after getting the basics working.
The combining operator is clearly a good thing since it gives us some
ability to do multiple inheritance of records.
Ben Chambers
every type 't in order for var to be *really* useful.
On Oct 5, 3:06 pm, "Christopher Diggins" <cdigg...@gmail.com> wrote: