小编luo*_*990的帖子

我被告知在依赖类型系统中,"类型"和"值"是混合的,我们可以将它们都视为"术语".

但是有一些我无法理解的东西:在没有Dependent Type(如Haskell)的强类型编程语言中,在编译时决定(推理或检查)类型,但是在运行时决定(计算或输入)值.

我认为这两个阶段之间肯定存在差距.试想一下如果从STDIN以交互方式读取一个值,我们如何在必须决定AOT的类型中引用该值？

例如,我需要从STDIN中读取一个自然数n和一个自然数列表xs(包含n个元素),如何将它们放入数据结构中Vect n Nat？

有filter : (a -> Bool) -> List a -> List aList,但是没有filter : (a -> Bool) -> Stream a -> Stream aStream,为什么？

是否有一些替代方案可以完成类似的工作？

到达错误分支时生成调用堆栈会花费运行时间；这很容易理解。

但是HasCallStack约束还会影响正常分支的性能吗？怎么样？

当我在这里阅读Church Rosser II定理时

定理(Church Rosser II)

如果有一个终止减少,那么最外面的减少也将终止.

我想知道:是否有一些定理加强了教会Rosser II定理,以便它告诉渐近时间复杂度而不是终止？

或者,是否可以证明所需减少策略在所有减少策略中具有最小的渐近时间复杂度？

我发现Lazy并Inf非常接近:

Lazy和Inf密切相关(事实上,底层实现使用相同的类型).实践中唯一的区别在于整体检查,其中Lazy被删除(即通常检查术语是否终止,忽略懒惰注释),Inf使用生产力检查器,其中任何延迟的使用必须是构造函数保护.

如所描述的以上,底层实现Lazy和Inf是同一个,唯一的区别是大约整体检查.

我认为总是使用Inf似乎更自然,这更接近我们在Haskell中使用的懒惰,并想知道我们必须使用的生产场景是什么Lazy- 它总是进行深度整体检查？

我发现,当我使用该stack new the-project-name new-template命令时,会在新目录中生成许多文件.我注意到以下4个特殊文件:

package.yaml
stack.yaml
Setup.hs
the-project-name.cabal

这4个文件似乎打算为软件包管理软件提供元数据,但它们看起来很混乱,我的意思是,为什么有4个,为什么不只是一个,它们之间有什么区别？

我们经常使用类型依赖来模拟子类型关系.

例如:

当我们想在OOP中表达Animal,Reptile和Aves之间的子类型关系时:

abstract class Animal {
    abstract Animal move();
    abstract Animal hunt();
    abstract Animal sleep();
}

abstract class Reptile extends Animal {
    abstract Reptile crawl();
}

abstract class Aves extends Animal {
    abstract Aves fly();
}

我们可以将上面的每个抽象类翻译成Haskell中的一个类型类:

class Animal a where
    move :: a -> a
    hunt :: a -> a
    sleep :: a -> a

class Animal a => Reptile a where
    crawl :: a -> a

class Animal a => Aves a where
    fly :: a -> …

我正在尝试定义一个名为的函数byteWidth,它捕获有关"获取特定原子类型的字节宽度"的用法.

我的第一次试用:

byteWidth : Type -> Int
byteWidth Int = 8
byteWidth Char = 1

并且Idris编译器抱怨:"当检查byteWidth的左侧时:左侧没有显式类型:Int"

我的第二次试验:

interface BW a where
  byteWidth : a -> Int

implementation BW Int where
  byteWidth _ = 8

implementation BW Char where
  byteWidth _ = 1

在这种情况下,我只能使用byteWidth,byteWidth 'a'但不能byteWidth Char.

我试图在 Idris 中导出 Show、Eq、Ord 等，但以下试验均无效：

踪迹#1：

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show)

得到：

deriving.idr:5:15-18:
  |
5 |     deriving (Show)
  |               ~~~~
When checking type of Main.Add:
Type mismatch between
        Type -> Type (Type of Show)
and
        Type (Expected type)

踪迹#2：

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show _)

得到：

*deriving> Lit 1
Lit 1 : Expr
*deriving> Add (Lit 1) (Lit 1)
(input):Can't infer argument …

AFAIK，有两种方法可以获取调用堆栈以在Haskell中进行调试：

1. HasCallStack在代码中添加约束
2. 用编译代码 ghc -prof -fprof-auto-top

我的测试代码：

import GHC.Stack

-- | a wrapper function to make "last" from base traceable
last' :: HasCallStack => [a] -> a
last' xs = case xs of [] -> error "abuse last"; _ -> last xs

-- | a untraceable partial function
foo :: [Int] -> Int
foo xs = last' xs + 1

-- | a untraceable partial function
-- , which looks like traceable, but it's call stack is cut off …