当前在线人数11702
首页 - 分类讨论区 - 电脑网络 - 葵花宝典版 - 同主题阅读文章

此篇文章共收到打赏
0

  • 10
  • 20
  • 50
  • 100
您目前伪币余额:0
未名交友
[更多]
[更多]
Hci, 物理量都是有单位的
[版面:葵花宝典][首篇作者:guvest] , 2019年05月13日23:01:18 ,372次阅读,16次回复
来APP回复,赚取更多伪币 关注本站公众号:
[分页:1 ]
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 1 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Mon May 13 23:01:18 2019, 美东)

从基本的原理来讲。物理量都有单位。物理理论允许的世界里,没有纯数。不然就会
允许把一个球的亮度和他的质量相加这样的操作。

所以现存的物理理论,实证了 数据加 “label/类型 ”系统的合理性。你
的论证有可取之处,但是太过宽泛。因为把你的论证当作一个模版,改几个字,就会得
出爱因斯坦是流水线上的工人,高斯是自由的手艺人这样的结论。






--
※ 修改:·guvest 於 May 14 00:08:14 2019 修改本文·[FROM: 47.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 2 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Mon May 13 23:28:19 2019, 美东)

话说回来。假如一个人认为做数论的比搞物理的更接近于自由的手艺人,也不能说是
mistake。因为这是个决定。也只是个决定。






--
※ 修改:·guvest 於 May 14 00:23:54 2019 修改本文·[FROM: 47.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
hci
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 3 ]

发信人: hci (海螺子), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Tue May 14 22:56:13 2019, 美东)

如RH所说,这些静态类型语言的问题就是没有单位。

静态类型推理能证明的东西,只限于计算机类型,这是个string,这是个list等等,对
人类用户没有任何意义。对人类有意义的名字,都被编译没了。

Clojure 里面,名字是用外显的Keyword 来表示的,不会被编译没了。

--
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 67.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 4 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 00:37:15 2019, 美东)

把float改名为kg。
把str改名为second。
在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头,你也可以下
棋。

纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由和学问。

发明clojure那
哥们讲的很多东西说实话我觉得他是半懂不懂。或者假装不懂。

从使用的角度批评现有的类型系统是一回事。从理论上否定类型我觉得没有太大的意义
。物理常数或
者单位把科学世界分为声光电磁热等等。你
不认可这个流水线方法是可以的。但那是个人为的选择,或者偏好。不是自然律,也和
道德律无关。


【 在 hci(海螺子) 的大作中提到: 】
<br>: 如RH所说,这些静态类型语言的问题就是没有单位。
<br>: 静态类型推理能证明的东西,只限于计算机类型,这是个string,这是个
list等
等,对
<br>: 人类用户没有任何意义。对人类有意义的名字,都被编译没了。
<br>: Clojure 里面,名字是用外显的Keyword 来表示的,不会被编译没了。
<br>




--
※ 修改:·guvest 於 May 15 01:02:20 2019 修改本文·[FROM: 47.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 5 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 00:55:06 2019, 美东)

基础的数据类型其实就是个单位。也就是说单位內存可以存幾個這樣類型的對象。
例如int的意思就是1 bit可以存1/8個int。

另外从反方面来讲。确有人认为物理规律应该是无单位的。
尽管没有work out 出来,也算是一门学问。

其实这个问题很有意思。我们想想看,神经网络可以fitting或者预测小的刚体球类型
的游戏的轨迹。它的单位在哪里?
这个问题似乎并不简单。因为神经网络对应的是nest起来的多项式。展开后的多项式,
系数就是单位。

Nest 多项式的系数和展开后的多项式的系数关系,不是线性的。总不能说好几个神经
网络的系数乘起来,共同拥有速度这个单位吧!

【 在 guvest(我爱你老婆Anna) 的大作中提到: 】
<br>: 把float改名为kg。
<br>: 把str改名为second。
<br>: 在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头
,你也
可以下
<br>: 棋。
<br>: 纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由
和学问。
<br>: 发明clojure那
<br>: 哥们讲的很多东西说实话我觉得他是半懂不懂。或者假装不懂。
<br>: 从使用的角度批评现有的类型系统是一回事。从理论上否定类型没有意义
。物理
常数或
<br>: 者单位把科学世界分为声光电磁热等等。你
<br>: 不认可这个流水线方法是可以的。但那是个人为的选择,或者偏好。不是
自然律
,也和
: ...................
<br>



--
※ 修改:·guvest 於 May 15 01:01:37 2019 修改本文·[FROM: 47.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
justnow
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 6 ]

发信人: justnow (阿材), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 01:59:32 2019, 美东)

类型的根本的作用是:决定 operator 的语义。比如 123 + 456 和 123 + "hello" 两
条表达式,同样是 + operator,但是语义完全不同,语义的决定完全取决于两个
operand 的类型。类型存在于语言或者运行环境层面,两者配合决定该如何执行一个运
算。

如果想进一步理解这些,你可以尝试写一个语言的编译器和运行环境 VM,就会明白一
个源码程序是怎样编译,并且在 VM 上面执行,实现语义的。

【 在 guvest (我爱你老婆Anna) 的大作中提到: 】
: 把float改名为kg。
: 把str改名为second。
: 在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头,你也可以下
: 棋。
: 纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由和学问。
: 发明clojure那
: 哥们讲的很多东西说实话我觉得他是半懂不懂。或者假装不懂。
: 从使用的角度批评现有的类型系统是一回事。从理论上否定类型我觉得没有太大的意义
: 。物理常数或
: 者单位把科学世界分为声光电磁热等等。你
: ...................




--
※ 修改:·justnow 於 May 15 02:02:38 2019 修改本文·[FROM: 47.]
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 7 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 02:22:53 2019, 美东)

在計算理論這方面,typed lambda calculus 1940年代就有了。無論從學理順序,還是
歷史順序看,编译器,vm什么的都是在计算理论基础上发展出来的技术。而不是反过来。

在數學裡面,type theory是羅素為了阻止悖論發明的。那是一戰以前了。

類型論和量綱分析的近似類比。是我的發明。不claim正確。
【 在 justnow(阿材) 的大作中提到: 】
<br>: 类型的根本的作用是:决定 operator 的语义。比如 123   456 和 123
  "
hello" 两
<br>: 条表达式,同样是   operator,但是语义完全不同,语义的决定完全取
决于两

<br>: operand 的类型。类型存在于语言或者运行环境层面,两者配合决定该如
何执行
一个运
<br>: 算。
<br>: 如果想进一步理解这些,你可以尝试写一个语言的编译器和运行环境 VM
,就会
明白一
<br>: 个源码程序是怎样编译,并且在 VM 上面执行,实现语义的。
<br>

--
※ 修改:·guvest 於 May 15 02:27:48 2019 修改本文·[FROM: 47.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 8 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 02:57:21 2019, 美东)

哦。找到更晚近的资料了。F sharp里面有。



http://typesatwork.imm.dtu.dk/material/TaW_Paper_TypesAtWork_Kennedy.pdf

这个作者90年代开始搞类型理论和量纲分析。

https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf) (文中的dimensional
的意思是中文的“量纲”)

应该是后来加进去F sharp里了。他这个
贴举的例子也是牛顿力学。

其实更早也有数学软件可以用类型来处理物理量的单位的。就是你在程序里可以直接写
1 kg,2 A等等。
但是理论发展一直比较慢。

看来我自己发明的类比,还是有可取之处的。
【 在 guvest(我爱你老婆Anna) 的大作中提到: 】
<br>: 在計算理論這方面,typed lambda calculus 1940年代就有了。無論從學
理順序
,還是
<br>: 歷史順序看,编译器,vm什么的都是在计算理论基础上发展出来的技术。
而不是
反过来。
<br>: 在數學裡面,type theory是羅素為了阻止悖論發明的。那是一戰以前了。
<br>: 類型論和量綱分析的近似類比。是我的發明。不claim正確。
<br>:


--
※ 修改:·guvest 於 May 15 03:06:39 2019 修改本文·[FROM: 47.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
justnow
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 9 ]

发信人: justnow (阿材), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 03:08:37 2019, 美东)

建议改一下,有些物理量没有单位的:
https://en.wikipedia.org/wiki/Dimensionless_physical_constant

【 在 guvest (我爱你老婆Anna) 的大作中提到: 】
: 从基本的原理来讲。物理量都有单位。物理理论允许的世界里,没有纯数。不然就会
: 允许把一个球的亮度和他的质量相加这样的操作。
: 所以现存的物理理论,实证了 数据加 “label/类型 ”系统的合理性。你
: 的论证有可取之处,但是太过宽泛。因为把你的论证当作一个模版,改几个字,就会得
: 出爱因斯坦是流水线上的工人,高斯是自由的手艺人这样的结论。



--
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 10 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 03:14:01 2019, 美东)

物理量我指的是测量出来的东西。用脚就叫foot。


【 在 justnow(阿材) 的大作中提到: 】
<br>: 建议改一下,有些物理量没有单位的:
<br>: https://en.wikipedia.org/wiki/Dimensionless_physical_constant
<br>
--
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 47.]

 
rgg
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 11 ]

发信人: rgg (rgg), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 09:44:02 2019, 美东)

F#走下坡路,市场没发展起来很遗憾。

【 在 guvest (我爱你老婆Anna) 的大作中提到: 】
: 哦。找到更晚近的资料了。F sharp里面有。
: http://typesatwork.imm.dtu.dk/material/TaW_Paper_TypesAtWork_Kennedy.pdf
: 这个作者90年代开始搞类型理论和量纲分析。
: (
: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf) (文中的
dimensional
: 的意思是中文的“量纲”)
: 应该是后来加进去F sharp里了。他这个
: 贴举的例子也是牛顿力学。
: 其实更早也有数学软件可以用类型来处理物理量的单位的。就是你在程序里可以直接写
: 1 kg,2 A等等。
: ...................



--
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 65.]

 
hci
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 12 ]

发信人: hci (海螺子), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 10:57:59 2019, 美东)

Isomorphism is insufficient for human use. Humans mostly care about identity
. Therefore automatic static typing is too weak to worth the cost it imposes
.


【 在 guvest(我爱你老婆Anna) 的大作中提到: 】
<br>: 把float改名为kg。
<br>: 把str改名为second。
<br>: 在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头,你也
可以下
<br>: 棋。
<br>: 纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由和学问。
<br>: 发明clojure那
<br>: 哥们讲的很多东西说实话我觉得他是半懂不懂。或者假装不懂。
<br>: 从使用的角度批评现有的类型系统是一回事。从理论上否定类型我觉得没有太大
的意义
<br>: 。物理常数或
<br>: 者单位把科学世界分为声光电磁热等等。你
: ...................
<br>
--
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 67.]

 
hci
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 13 ]

发信人: hci (海螺子), 信区: Programming
标  题: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 11:00:43 2019, 美东)

Kg cannot be changed into float without losing most of its information,
which is precisely what automatic static typing does.


【 在 guvest(我爱你老婆Anna) 的大作中提到: 】
<br>: 把float改名为kg。
<br>: 把str改名为second。
<br>: 在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头
,你也
可以下
<br>: 棋。
<br>: 纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由
和学问。
<br>: 发明clojure那
<br>: 哥们讲的很多东西说实话我觉得他是半懂不懂。或者假装不懂。
<br>: 从使用的角度批评现有的类型系统是一回事。从理论上否定类型我觉得没
有太大
的意义
<br>: 。物理常数或
<br>: 者单位把科学世界分为声光电磁热等等。你
: ...................
<br>

--
※ 修改:·hci 於 May 15 11:01:19 2019 修改本文·[FROM: 67.]
※ 来源:· 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 67.]

 
hci
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 14 ]

发信人: hci (海螺子), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Wed May 15 20:28:30 2019, 美东)

No response?

This is the crux of the matter.

【 在 hci (海螺子) 的大作中提到: 】
: Kg cannot be changed into float without losing most of its information,
: which is precisely what automatic static typing does.
: <br>: 把float改名为kg。
: <br>: 把str改名为second。
: <br>: 在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头
: ,你也
: 可以下
: <br>: 棋。
: <br>: 纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由
: 和学问。
: ...................



--
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 12.]

 
hci
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 15 ]

发信人: hci (海螺子), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Thu May 16 01:42:46 2019, 美东)

最关键的东西不予置评,算不算鸵鸟?

【 在 hci (海螺子) 的大作中提到: 】
: No response?
: This is the crux of the matter.



--
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 67.]

 
hci
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 16 ]

发信人: hci (海螺子), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Thu May 16 01:47:41 2019, 美东)

把“公斤”这个对人类有意义的词编译掉了, 只留下“浮点数”这个计算机类型,这
就是现代类型静态分析干的事,然后号称这就是对保证软件质量最重要的帮助了。

这不是扯鸡巴蛋是什么?

这就是静态类型扇子要让你们相信的扯淡。

【 在 hci (海螺子) 的大作中提到: 】
: Kg cannot be changed into float without losing most of its information,
: which is precisely what automatic static typing does.
: <br>: 把float改名为kg。
: <br>: 把str改名为second。
: <br>: 在比较远的代数抽象层上。都是一回事。这就好比把棋子拿掉,换成石头
: ,你也
: 可以下
: <br>: 棋。
: <br>: 纯数加上label这个想法,不管这个label是单位或者类型,有自己的理由
: 和学问。
: ...................



--
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 67.]

 
guvest
进入未名形象秀
我的博客
[回复] [回信给作者] [本篇全文] [本讨论区] [修改] [删除] [转寄] [转贴] [收藏] [举报] [ 17 ]

发信人: guvest (我爱你老婆Anna), 信区: Programming
标  题: Re: Hci, 物理量都是有单位的
发信站: BBS 未名空间站 (Thu May 16 10:14:30 2019, 美东)

我对自己的收获满意了。不需要再参与这些讨论。
等我仔细看看Terrance Tao那个blog,有空再说。
【 在 hci (海螺子) 的大作中提到: 】
: 最关键的东西不予置评,算不算鸵鸟?




--
※ 修改:·guvest 於 May 16 10:15:24 2019 修改本文·[FROM: 38.]
※ 来源:·WWW 未名空间站 网址:mitbbs.com 移动:在应用商店搜索未名空间·[FROM: 38.]

[分页:1 ]
[快速返回] [ 进入葵花宝典讨论区] [返回顶部]
回复文章
标题:
内 容:

未名交友
将您的链接放在这儿

友情链接


 

Site Map - Contact Us - Terms and Conditions - Privacy Policy

版权所有,未名空间(mitbbs.com),since 1996