5 ms·

> We know statically that its car is x, of symbol type. I'm saying within a statically typed Lisp or when trying to use HM's algorithm w you don't know what ty

by urs2102 11y ago

> We know statically that its car is x, of symbol type. I'm saying within a statically typed Lisp or when trying to use HM's algorithm w you don't know what type of car of (x y z). The type of "symbol" is not specific enough as what operations will you allow to be run on symbol if you're working in a statically typed Lisp with type inference. If symbol is a character you can't run a float addition on it, and any attempt to do so should throw an error at compile time. In the case above, I'm using x, y, and z as substitutes for characters, floating point numbers, integers, etc. I'm trying to see if I can figure out the specific type in compile time rather than runtime.

kazinator 11y ago
If we know that L is a list, and that is all we know, we don't know what type (car L) is. If we know that L holds the value (X Y Z), then we know that the type of (car L) is symbol. > The type of "symbol" is not specific enough It absolutely is specific enough. It's a fundamental type in the language. We just don't know what kind of symbol for certain purposes. If we only know that some object O is a symbol, we don't know whether whether it is self-evaluating (nil, t, keyword symbols in CL) or bindable (any other symbol). In this particular case, not only do we know that (car L) is of type symbol, we know which symbol!!! We know the exact identity of the object: it is X. If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information. > as what operations will you allow to be run on symbol if you're working in a statically typed Lisp with type inference If I know that O is a symbol, then we can, for instance, compile the (symbol-name O) operation such that O's type tag isn't checked; however, if there is a special representation for a symbol nil, we have to distinguish that. In this case we know that X isn't nil. > If symbol is a character ... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect. What Lisp tutorial have you been following? Perhaps you have confused symbol objects, and the use of a symbol as a variable name (X having a value binding in a given environment, and the value of that binding being a character object).
- urs2102 11y ago
  Oh perhaps I'm not being specific enough. Apologies mate. > If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information. By '(x y z) I'm assuming that it's not a quoted list literal but a let's say list generated by a function at compile time. Where x, y, and z could be of different types like ('(2.5 7) 6 "hello"). It's very hypothetical, and the contents of the list generated cannot possibly be known at compile time. > ... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect. And yes, what I'm talking about is building a toy lisp between an ML language and a Lisp to see how much Lispyness you have to trade off for the static typing and the type inference of an ML language. The definition of oddball! In OCaml for example which has static typing and type inference you can't just have a "symbol". Even though symbols are a basic part of Lisp, you can't have really strong type inference for a "symbol" despite it being a fundamental type in the language as for strong type inference you would want to do stuff like have separate operators for adding integers and adding floating point numbers. This is very important for HM's algorithm w, similarly - in that case, car needs to be able to take one type, and return one type for it to comply with algorithm w. I'm trying to see if other people had ever tried implementing something like this. Anyway, great conversation! I think DonaldFisk helped me out already, but thanks!

by urs2102 11y ago

kazinator 11y ago

If we know that L is a list, and that is all we know, we don't know what type (car L) is. If we know that L holds the value (X Y Z), then we know that the type of (car L) is symbol. > The type of "symbol" is not specific enough It absolutely is specific enough. It's a fundamental type in the language. We just don't know what kind of symbol for certain purposes. If we only know that some object O is a symbol, we don't know whether whether it is self-evaluating (nil, t, keyword symbols in CL) or bindable (any other symbol). In this particular case, not only do we know that (car L) is of type symbol, we know which symbol!!! We know the exact identity of the object: it is X. If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information. > as what operations will you allow to be run on symbol if you're working in a statically typed Lisp with type inference If I know that O is a symbol, then we can, for instance, compile the (symbol-name O) operation such that O's type tag isn't checked; however, if there is a special representation for a symbol nil, we have to distinguish that. In this case we know that X isn't nil. > If symbol is a character ... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect. What Lisp tutorial have you been following? Perhaps you have confused symbol objects, and the use of a symbol as a variable name (X having a value binding in a given environment, and the value of that binding being a character object).

urs2102 11y ago
Oh perhaps I'm not being specific enough. Apologies mate. > If we know this at compile time, because L is a quoted list literal, we have the strongest possible information about what it is, even more precise than most type information. By '(x y z) I'm assuming that it's not a quoted list literal but a let's say list generated by a function at compile time. Where x, y, and z could be of different types like ('(2.5 7) 6 "hello"). It's very hypothetical, and the contents of the list generated cannot possibly be known at compile time. > ... then you're talking about a completely different language that isn't one of the mainstream Lisps. At best a very oddball dialect. And yes, what I'm talking about is building a toy lisp between an ML language and a Lisp to see how much Lispyness you have to trade off for the static typing and the type inference of an ML language. The definition of oddball! In OCaml for example which has static typing and type inference you can't just have a "symbol". Even though symbols are a basic part of Lisp, you can't have really strong type inference for a "symbol" despite it being a fundamental type in the language as for strong type inference you would want to do stuff like have separate operators for adding integers and adding floating point numbers. This is very important for HM's algorithm w, similarly - in that case, car needs to be able to take one type, and return one type for it to comply with algorithm w. I'm trying to see if other people had ever tried implementing something like this. Anyway, great conversation! I think DonaldFisk helped me out already, but thanks!