小编Nou*_*are的帖子

连贯性是什么意思?

在Simon Peyton Jones、Mark Jones 和 Erik Meijer的论文“类型类:探索设计空间”中,他们非正式地定义了连贯性如下:

程序的每个不同的有效类型派生都会导致具有相同动态语义的结果程序。

首先,程序没有类型;表达式、变量和函数都有类型。所以我想我会把它解释为每个程序片段(表达式、变量或函数)必须有一个唯一的类型派生。

那么我想知道Haskell(说Haskell2010)是否真的连贯?例如,表达式\x -> x可以被赋予类型a -> a,但也可以被赋予Int -> Int。这是否意味着连贯性被打破了?我能想到两个反驳:

  1. Int -> Int不是有效的类型派生,该术语\x -> x获得推断类型a -> a,它比Int -> Int.

  2. 两种情况下的动态语义是相同的,只是类型Int -> Int不太通用,在某些上下文中会被静态拒绝。

其中哪些是真的?还有其他反驳吗?

现在让我们考虑类型类,因为在该上下文中经常使用一致性。

GHC 实现的 Haskell 可能通过多种方式破坏一致性。显然,IncoherentInstances扩展和相关的INCOHERENTpragma 似乎是相关的。孤儿实例也会浮现在脑海中。

但是如果上面的第 1 点是真的,那么我会说即使这些也不会破坏一致性,因为我们可以说 GHC 选择的实例是应该选择的一个真实实例(并且所有其他类型的派生都是无效的) ),就像 GHC 推断的类型是必须选择的真实类型一样。所以第1点可能不是真的。

然后还有更多看似无辜的扩展,例如通过OverlappingInstances扩展或Overlapping,OverlapsOverlappablepragma重叠实例,但即使是MultiParamTypeClasses和的组合也FlexibleInstances可能产生重叠实例。例如

class A a …
Run Code Online (Sandbox Code Playgroud)

haskell type-systems ghc

8
推荐指数
1
解决办法
117
查看次数

解决“c-source”名称和 GHC RTS 名称之间的冲突

我有一些使用 FFI 从 Haskell 调用的 C 源代码ccall。为了使构建过程尽可能简单,我想使用 Cabal 编译 C 文件,因此我已将源代码添加到c-sources我的.cabal文件部分。

问题是我导入 Haskell 的 C 函数是根据另一个名为 的 C 函数(我没有直接从 Haskell 使用)来实现的allocate,这会导致链接时发生冲突:

ratkai> [16 of 16] Linking .stack-work/dist/x86_64-linux/Cabal-3.8.1.0/build/ratkai-tvc/ratkai-tvc [Objects changed]
ratkai> /usr/bin/ld.gold: error: /home/cactus/.ghcup/ghc/9.4.5/lib/ghc-9.4.5/lib/../lib/x86_64-linux-ghc-9.4.5/rts-1.0.2/libHSrts-1.0.2.a(Storage.o): multiple definition of 'allocate'
ratkai> /usr/bin/ld.gold: .stack-work/dist/x86_64-linux/Cabal-3.8.1.0/build/ratkai-tvc/ratkai-tvc-tmp/import/ZX0/src/memory.o: previous definition here
ratkai> collect2: error: ld returned 1 exit status
ratkai> ghc-9.4.5: `gcc' failed in phase `Linker'. (Exit code: 1)
Run Code Online (Sandbox Code Playgroud)

有没有办法解决这个问题,而无需修补导入的 C 库来重命名其allocate函数

linker haskell ffi ghc

6
推荐指数
0
解决办法
46
查看次数

Haskell RankNTypes - 功能域的限制

不明白为什么会这样,指的是:Rank2Types的目的是什么?-> @dfeuer 解释:

... 要求参数是多态的不仅允许它与多种类型一起使用;它还限制了该函数可以用它的参数做什么以及它如何产生它的结果......

f :: (forall a . [a] -> a) -> IO ()
Run Code Online (Sandbox Code Playgroud)

...事实上,没有函数返回不在给定列表中元素会进行类型检查

在对 rank-N 类型的任何解释中,我都没有看到这种效果(或好处)的描述,大部分时间是关于让被调用者选择类型等的故事......这对我来说很清楚并且易于掌握但是我看不出我们可以通过哪种美德(仅扩展等级)来控制/限制功能域(和共域)...

如果有人可以更深入地了解此处涉及的 rankN 机制。谢谢

polymorphism haskell rank-n-types

3
推荐指数
1
解决办法
55
查看次数

为什么 Haskell 不接受列表的这种语法?

考虑以下 Idris 中的代码片段:

myList : List Int
myList = [
  1,
  2,
  3
]
Run Code Online (Sandbox Code Playgroud)

结束定界符]与声明本身位于同一列。我发现这是一种很自然的方式来格式化长的多行列表。

但是,Haskell 中的等效代码段无法编译并出现语法错误:

myList :: [Int]
myList = [
  1,
  2,
  3
]

>>  main.hs:9:1: error:
>>     parse error (possibly incorrect indentation or mismatched brackets)?
>>   |
>> 9 | ]
>>   | ^
Run Code Online (Sandbox Code Playgroud)

并且要求将结束定界符]放置在严格大于表达式声明位置的列号上。或者至少,据我所知,这似乎是正在发生的事情。

Haskell 不喜欢这种语法有什么原因吗?我知道 Haskell 解析器和词法分析器之间存在一些微妙的交互,以启用 Haskell 的越位规则实现,所以也许它与此有关。

haskell

1
推荐指数
1
解决办法
125
查看次数

Haskell 中奇怪的变量绑定

我在 Haskell 中有以下代码,它是 Brainfuck 解释器的一部分(当我学习一门新语言时,我最喜欢的第一个中型项目):


type Program = String
type Pointer = Int
type Stack = [Int]

data ExecutionState = ExecutionState {
  programPointer :: Pointer,
  program :: Program,
  stackPointer :: Pointer,
  stack :: Stack
} deriving (Eq, Show)

moveBackwards :: ExecutionState -> ExecutionState
moveBackwards (ExecutionState pp p sp s) = ExecutionState (pp-1) p sp s

curr :: ExecutionState -> Char
curr execState = (stack execState) !! (stackPointer execState)

currByte :: ExecutionState -> Int
currByte execState = (program execState) !! (programPointer …
Run Code Online (Sandbox Code Playgroud)

haskell

1
推荐指数
1
解决办法
185
查看次数

将 f 应用于每个元素并将结果作为列表返回

我希望我的函数someZip返回应用于f每个元素的结果列表。

这是我到目前为止得到的:

someZip :: (a -> b -> c -> d) -> [(a,b,c)] -> [d]
someZip f (x:xs) (y:ys) (z:zs)  = f x y z : someZip f xs ys zs
Run Code Online (Sandbox Code Playgroud)

我尝试了不同的方法,但找不到解决此问题的方法。我现在完全迷失了,我在这里错过了什么?

haskell

-1
推荐指数
1
解决办法
67
查看次数

标签 统计

haskell ×6

ghc ×2

ffi ×1

linker ×1

polymorphism ×1

rank-n-types ×1

type-systems ×1