m****o
发帖数: 182 | 1 长期写强类型语言影响，看到M x N 编译器无法自动检查矩阵形状是否匹配总觉得全身
不自在。Idris可以直接把矩阵形状编制成类型变量，比如类型Matrix Double 5 2代表
一个双精度浮点5行2列矩阵类型，那么矩阵乘法function就可以定义成如下，
mul : Num n => Matrix n a b -> Matrix n b c -> Matrix n a c
mul = ???
这样定义矩阵乘法对于我这种类型强迫症是一个极大的relief：编译阶段就可以自动检
测矩阵形状不匹配错误，并且程序可读性也会增加。大家怎么看？ |
g****t
发帖数: 31659 | 2 这个语言还不错啊，看得出来作者认真考虑和设计过。但文档里自己写了，没有
resource,不是production ready的。
另外这个和机器学习不是等价比较吧 |
g****t
发帖数: 31659 | 3 看了下作者简介。作者phd写这个题目到现在这个实现
也有10年时间积累，难怪我看着质量挺高的。
改天有空我玩玩
: 这个语言还不错啊，看得出来作者认真考虑和设计过。但文档里自己写了
，没有
: resource,不是production ready的。
: 另外这个和机器学习不是等价比较吧
【在 g****t 的大作中提到】
: 这个语言还不错啊，看得出来作者认真考虑和设计过。但文档里自己写了，没有
: resource,不是production ready的。
: 另外这个和机器学习不是等价比较吧
|
m****o
发帖数: 182 | 4 不是等价，但是如果有人愿意造轮子的话，肯定有竞争力，毕竟机器学习大量的操作都
牵涉到矩阵。
【在 g****t 的大作中提到】
: 这个语言还不错啊，看得出来作者认真考虑和设计过。但文档里自己写了，没有
: resource,不是production ready的。
: 另外这个和机器学习不是等价比较吧
|
L****8
发帖数: 3938 | 5 eigen c++ 不好用么？
【在 m****o 的大作中提到】
: 长期写强类型语言影响，看到M x N 编译器无法自动检查矩阵形状是否匹配总觉得全身
: 不自在。Idris可以直接把矩阵形状编制成类型变量，比如类型Matrix Double 5 2代表
: 一个双精度浮点5行2列矩阵类型，那么矩阵乘法function就可以定义成如下，
: mul : Num n => Matrix n a b -> Matrix n b c -> Matrix n a c
: mul = ???
: 这样定义矩阵乘法对于我这种类型强迫症是一个极大的relief：编译阶段就可以自动检
: 测矩阵形状不匹配错误，并且程序可读性也会增加。大家怎么看？
|
m****o
发帖数: 182 | 6 支持dependent object type吗？
【在 L****8 的大作中提到】
: eigen c++ 不好用么？
|
n*w
发帖数: 3393 | 7 目前是不是还没有任何主流语言支持这个type？
【在 m****o 的大作中提到】
: 支持dependent object type吗？
|
m****o
发帖数: 182 | 8 Scala从dotty compiler开始将支持dependent object type，这也是dotty取名的由来
。Scala在一路向太阳系最复杂语言目标狂奔。
【在 n*w 的大作中提到】
: 目前是不是还没有任何主流语言支持这个type？
|
g****t
发帖数: 31659 | 9 能介绍下你用这个Idris的tool chain是什么？Editor，库，什么的？
假设我想写一个AX=B的加自定义regulation的recursive最小二乘法。
我有时间的话，试试看回来跟大家汇报
【在 m****o 的大作中提到】
: Scala从dotty compiler开始将支持dependent object type，这也是dotty取名的由来
: 。Scala在一路向太阳系最复杂语言目标狂奔。
|
m****o
发帖数: 182 | 10 暂时还没这方面的轮子啊。editor方面和Haskell一样，直接上vim就可以了。你要是感
兴趣的话，Manning最近出了本书：
https://www.manning.com/books/type-driven-development-with-idris
大家可以一起学着玩一下。
【在 g****t 的大作中提到】
: 能介绍下你用这个Idris的tool chain是什么？Editor，库，什么的？
: 假设我想写一个AX=B的加自定义regulation的recursive最小二乘法。
: 我有时间的话，试试看回来跟大家汇报
|
n*w
发帖数: 3393 | 11 支持这个的学术性研究性语言倒是有好几个。
【在 m****o 的大作中提到】
: Scala从dotty compiler开始将支持dependent object type，这也是dotty取名的由来
: 。Scala在一路向太阳系最复杂语言目标狂奔。
|
d*******r
发帖数: 3299 | 12 以后搞AI搞公式多的话，这些个FP语言会不会搭上个便车?
【在 m****o 的大作中提到】
: 长期写强类型语言影响，看到M x N 编译器无法自动检查矩阵形状是否匹配总觉得全身
: 不自在。Idris可以直接把矩阵形状编制成类型变量，比如类型Matrix Double 5 2代表
: 一个双精度浮点5行2列矩阵类型，那么矩阵乘法function就可以定义成如下，
: mul : Num n => Matrix n a b -> Matrix n b c -> Matrix n a c
: mul = ???
: 这样定义矩阵乘法对于我这种类型强迫症是一个极大的relief：编译阶段就可以自动检
: 测矩阵形状不匹配错误，并且程序可读性也会增加。大家怎么看？
|
