-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[ANNOUNCEMENT] Static Typecheck & Type Inference #486
Comments
初读,感觉“量”这个字不太好。 比较读一下: 还有一点,“数言列爻物”读来都是比较具象的名词,但“量”就突然抽象了。“器”也是具象的名字,又可通用。 |
It doesn't work for function parameter of object type. Code:
Error message:
Output:
|
@lymslive , thanks for the suggestion! Polymorphic types are meant to sound abstract, because they ARE abstract ideas. I agree that 量 may not necessarily be the best word, but I don't think 器 is a big improvement either. Like you said, 器 could mean containers, and user might easily confuse with container types, such as arrays, objects, etc. 量 seems like a word commonly used to denote unspecified types, e.g. 標量 向量 应/自變量. I've also considered other words such as 元, 端, 象, 實. As always, I'm happy to hear more wording suggestions. |
@statementreply , thanks for spotting the bug! I'll look into it right away. |
@LingDong- “標量 向量 应/自變量” 这几个词都是现代汉语词汇,所以我才说会有出戏感。 |
Notice that 容器 is also a relatively modern word. 器 is more commonly used in classical times to mean containers. Like you mentioned in your other post, those early translators of western concepts into the Chinese language are well-versed in Classical Chinese. 意譯, unlike 音譯, often draw inspiration from the traditional usage of words. I think the tricky problem of translating the concept of "variable" is to certain extent solved by those who came before us. Unless there is an enormous advantage, there is not much need to reinvent. |
@statementreply , the bug is now fixed in the newest commit 182d100 It should now compile without errors and spit out the (more) correct signature:
Theoretically the Implementation detail: For Thanks again for spotting the bug! Let me know if this (or any other) issue remains. |
@LingDong- You mean not understand the underlying thought of “形上谓之道,形下谓之器” quiet well. I just think the two concept in it can map to the key concenpt of progromming world well: algorithm(function) and data struct(variable), where function if implement or wrapper of algorithm, and variable can represent or reference data struct. We've used “术" to express function concept, that's good and can found it's origin from 《九章算术》and other math books. It's meaning is close to “道", but ”道" occupies on a higher level, that may corresponding to algorithm in programming. That's why I prefer "器" to express variable concept. By the way, ”象" is also acceptable, it origin from 《易经》。“易” not means random, but changing, that's also close to variable concept in some aspect。 If you really dislike “器” for variable, you may used for class. Though I donot think you have to implement the full complex of class. OOP is not best nowadays. |
I got the same result and error messages. It appears to me that the commit 182d100 contains only changes to test code. |
@lymslive , I think it is actually great to have an in-depth discussion on keywords, as they’re integral parts of the language. It is better to make good decision on keywords now, than to have the pain of changing them later. I am totally aware of the meaning of 形上谓之道,形下谓之器, and I enjoyed the way you interpreted it from programming perspective. Similarly, you’re definitely not the only person who love 易經. However, to supplement what I already said, although 器 could be used in this abstract way, once you put a numeral before it, e.g. 吾有二器, it starts to have a concrete meaning, and to readers, this probably means instrument or container. As for the other keywords I mentioned earlier, here are some thought process.
Here’s another idea. Instead of using pre-Qin philosophical terminology, maybe we can also consider going for the 傳奇戲曲 style, using 奇 and 寶 for the types we not yet know what they actually are. e.g. 吾有一奇 or 必先得一寶. More light-hearted, but could also work. This discussion is rather unexpected since this post is mainly about static type inference and the benefits it brings for the language (which nobody seems to care :), but I think keywords are equally important. I’ll consider more about this, and let you know if I ever decide to change it. |
@statementreply Oops, I committed in the wrong folder (again :). It should be fixed now with this fresh commit: 0195caa , thanks! |
@LingDong-
Then I want to talk about another topic. I think you don't worry about the problem with “吾有二”. In traditional Chinese, “吾有一物” not means "I have one" exactly, but "I have a" or just "I have", or "I have the object named ...". So it hardly extend this pattern only increase the apparent number “一” to “二” or “三”. If we really want define multiple variable in one statement, we may say multiple “一”, such as Sometimes only “一” can express the meaning "have", I still remember in one textbook has a sentence “一桌一椅一抚尺而已”. "一" is much more meaningful than number "one" in traditional Chinese. Then I suddenly think up that wan only use “一” to express the unknown type variable, just omit the type keyword if unknown or hardly describe exactly.
Since it's type is unknown, it's value must be undefined either, so no need to say “曰” any more. Addition argue “一” to “二” comes from “术”. We can only define “吾有一术”, but nearly unreadable to say “吾有二术”. So we should depress using “吾有二” to define normal variable type, only encourage “吾有一” consistently. Otherwise new comer definitely will ask how to define “吾有二术” as “吾有二物”. Hope helpful fro you. 怎么说呢,虽然“吾有二数”比“吾有一数”多了一数,但它的“逼格”降了不止一个数量级。 |
周棄曰。少昊有四叔。曰重。曰該。曰修。曰熙。 吳王壽夢有四子。長曰謁。次曰餘祭。次曰夷昧。次曰季札。 以荒政十有二聚萬民:一曰散利,二曰薄徵,三曰緩刑,四曰弛力,五曰捨禁,六曰去幾,七曰眚禮,八曰殺哀,九曰蕃樂,十曰多昏,十有一曰索鬼神,十有二曰除盜賊。 凡祭有四時:春祭曰礿,夏祭曰禘,秋祭曰嘗,冬祭曰烝。 子夏曰。君子有三變。望之儼然。即之也溫。聽其言也厲。 故言必有三表。何謂三表。子墨子言曰。有本之者。有原之者。有用之者。 孔子曰。人有五儀。有庸人。有士人。有君子。有賢人。有聖人。 :) |
Yes, many usage can be found in traditional Chinese book, but we have to Actually in my last post the mainly purpose is to provide another solution for In my opinion, repeat “一” is more simple and handy than “曰”. And someone In programming world, it is better to distinguish literal number and keyword, When a programmer can write “吾有二数” and “吾有三数”, he may also, in theory, Then refer to the syntax of “术”, for argument, your first design is “必先得六
It seams to have tow syntax pattern for tow same type argument, and much more |
Sorry to contradict, but I think the current mechanism makes sense. As stated in the 1st line of the Feature section of the README, one of the goals of wenyan-lang is to simulate the natural language used by the ancient Chinese people. It is one of the fundamental reasons this project exists at all. To supplement my examples taken from the classics, here is a simpler example for you: when you're cooking stir-fried tomatos and scrambled eggs, you would say I need five eggs and two tomatos. You wouldn't say I need a tomato, I need a tomato, I need an egg, I need an egg, I need an egg, I need an egg, I need an egg. This is why we have 必先得五數曰⋯⋯二言曰⋯⋯ When in doubt, please assume the language features are carefully planned, thought out and implemented, and not rashly put together and "patched" later. Then we can have a more meaningful discussion about how to improve them further. I would really appreciate it, thanks! |
Yes, current syntax make sense, that why I'm here and cannot restrain myself to discuss with you in detail, or too detail. But I don't think your cook example above match what I mean exactly. If you need two tomatos and five eggs, it will be Only when the elements, say the five eggs can be distinguished from each other or have different purpose in the cook, then we can name them separately, for example, 生鸡蛋,熟鸡蛋,鸭蛋,鹌鹑蛋,凤凰蛋. In this case, we can list them one by one. Of course we can first announce the summary count, then list each after that. Actually this is current syntax in wenyan-lang.
It is supposed we have a type “蛋”, or make “蛋” generic type keyword. What I means is that we can also omit the summary prefix “五蛋”, only list each different variables which may belong to type “蛋”.
This is also valid grammar in traditional Chinese, and in some context it may have more 文采 than plain 曰. Now that we don't have type “蛋”, and impossible use it as generic or unknown type, then we have to say with another keyword, for example:
In my option, any candidate keyword sound strange. So I propose just omit the prefix summary count and unknown type. While in concrete type case, it is still nice optionally prefix with summary count and postfix with value. Another trivial benefit omit summary count number is a bit easier to modify code, if we add or delete another “蛋”, we only need modify one place, no need to remember modify to count accordingly. It will let programmer make less mistake in practical coding. I think one purpose of strong type/check is also advancing to practical coding, make programmer less mistake. Sorry my post may pollute this issue. I also expect more technique discussion under this issue. |
I think omitting type for polymorphic types using |
As another step toward a strongly-typed language with a functional flavor, wenyan-lang now supports ML style static typechecking and inference. When the option is turned on, the compiler will now raise exceptions if your code does not typecheck. Also it is capable of producing type signatures for inspection, e.g.
./example/quicksort.wy
produces the following:Each scope is wrapped by indentation and
{}
. The numbers in[]
are character ranges of the scope in the source file.wenyan-lang uses bi-directional type inference. For example, when it reads that you declared an array, it will be recognized as a polymorphic array
'a arr
(alpha-array). It then reads on to find out, say, you're pushing numbers into it, it automatically turns the array into anum arr
. Similarly when you start doing multiplication*
with two polymorphic types, it will realize that these types must have beennum
s and change accordingly.When you have not done anything explicit to hint the type of the array, it will stay as polymorphic. This is very useful if your function should work for any array, e.g. reversing, sorting, splitting, etc.
Usage
Since this feature is still experimental, it is turned off by default. You can turn it on by changing the
strict
flag totrue
forparser.compiler
. Imported libraries will not be checked to avoid flooding the log, but all the standard libraries is already known to pass all the typechecks so you don't need to worry.Motivation
This kind of type inference is very suitable for wenyan-lang, because explicit type declarations are not very readable in natural language.
数列
is fine,数列列列
is harder to read, and if your type signature involve any kind of nested structure, it will not be possible to express without the aid of brakcets, (e.g.数 -> (数->数列) -> 数
, is different from, say,数 -> (数->数) 列 -> 数
). In comparison, the static type inference system only requires you to be self-consistent, achieving type safty without your labor of spelling out all the types.Details
let
inJavaScript
. Some examples in the./example
folder assumed function scope, and have already been corrected for.量
. You can use it like any other type, e.g.吾有一量
or必先得一量曰「甲」
. This is the generic/polymorphic/any type, a bit similar toC++
auto
.Limitations
'a->'b
type for a function that has not been declared, and progressively infer the type based on that. More ideally, in the future it will search the same scope and lift the defination to top, and raise errors if none can be found. Another solution is to separate declarations and definitions like C/C++, which requires a header-like listing of functions at the top of the file (inconvenient).'a
type, currently it does not trace into the imported module and run inference on everything to figure out.x : 'a arr
andy : 'b arr
. If you started putting items fromx
intoy
, ideally the checker should realize'a
and'b
must be the same thing, and generate signaturex : 'a arr, y : 'a arr
. Currently, all the'a
'b
labelling in the type signature are aribtrary, they're all just equally generic.Example
Here is the type signature of the turing machine example
./example/turing.wy
. Notice how 2 dimensional arrays are inferred, when user only anotated them as列
.There is still some work to be done to hone this type system, but I hope one day it will be as good as Haskell or SML. Maybe in the extremely distant future we'll be able to make a formal verification :)
Please let me know if you find any issues, and feel free to discuss in the comments!
The text was updated successfully, but these errors were encountered: