小编Rol*_*oly的帖子

我可能在这里错过了一些愚蠢的东西.我认为元组类型[string, number]大致相当于union-of-union类型(string | number)[],因此以下是合法的:

function lengths (xs: string[]): [string, number][] {
   return xs.map((x: string) => [x, x.length])
}

然而,tsc 1.4抱怨:

Config.ts(127,11): error TS2322: Type '(string | number)[][]' is not assignable to type '[string, number][]'.
  Type '(string | number)[]' is not assignable to type '[string, number]'.
    Property '0' is missing in type '(string | number)[]'.

我究竟做错了什么？

已经说明了所有agda程序终止的几个地方.但是我可以构造一个这样的函数:

stall : ? n ? ?
stall 0 = 0
stall x = stall x

语法高亮显示器似乎不喜欢它,但没有编译错误.

计算stall 0结果的正常形式0.计算结果stall 1导致Emacs挂起看起来很像非终止循环.

这是一个错误吗？或者Agda有时会永远运行？或者是更微妙的事情？

我似乎在尝试从源代码构建它的过程中破坏了我在Ubuntu 13.10上的TypeScript安装.我已经放弃了,现在只想回到工作二进制安装.

我删除了NodeJS --purge并重新安装了via

sudo apt-get install nodejs

并确保'node'确实指向NodeJS(而不是我卸载的Ubuntu包"node").打字node在命令行滴我到提示的NodeJS,这样看起来不错.

然后我重新安装npm,然后通过TypeScript二进制文件

sudo npm -g install TypeScript@0.9.1-1

结果导致了

npm http GET https://registry.npmjs.org/typescript/0.9.1-1
npm http 304 https://registry.npmjs.org/typescript/0.9.1-1
/usr/local/bin/tsc -> /usr/local/lib/node_modules/typescript/bin/tsc
typescript@0.9.1-1 /usr/local/lib/node_modules/typescript

我查了which tsc点/usr/local/bin/tsc.该文件的内容是:

#!/usr/bin/env node
require('./tsc.js')

该目录/usr/local/lib/node_modules/typescript/bin/包含

drwxr-xr-x  3 nobody rolyp    4096 Oct 24 22:55 ./
drwxr-xr-x  3 nobody rolyp    4096 Oct 24 22:55 ../
-rw-r--r--  1 nobody rolyp  323793 Aug 21 17:17 lib.d.ts
drwxr-xr-x 16 nobody rolyp    4096 Oct 24 …

我已经使用Agda 9个月了.我第一次发现自己想要"运行"(作为顶级可执行文件)打印字符串的Agda程序.叫我老式的.

我可以编写一个程序来计算字符串并让Agda 在交互模式(或Emacs)中向我显示字符串的值.但字符串很长并且嵌入了换行符.我希望它实际打印出来.

通过比较,在GHCi中,我可以这样做:

Prelude> putStrLn "hello, world!"
hello, world!

但是在Agda的交互模式中我得到了这个:

Main> putStrLn "hello, world!"
.IO.?-15
('h' .Data.Colist.Colist.?
 .Data.Colist.?-2 'h'
 ('e' .Data.List.List.?
  'l' .Data.List.List.?
  'l' .Data.List.List.?
  'o' .Data.List.List.?
  ',' .Data.List.List.?
  ' ' .Data.List.List.?
  'w' .Data.List.List.?
  'o' .Data.List.List.?
  'r' .Data.List.List.?
  'l' .Data.List.List.?
  'd' .Data.List.List.? '!' .Data.List.List.? .Data.List.List.[]))
>>
.IO.?-16
('h' .Data.Colist.Colist.?
 .Data.Colist.?-2 'h'
 ('e' .Data.List.List.?
  'l' .Data.List.List.?
  'l' .Data.List.List.?
  'o' .Data.List.List.?
  ',' .Data.List.List.?
  ' ' .Data.List.List.?
  'w' .Data.List.List.?
  'o' .Data.List.List.?
  'r' .Data.List.List.?
  'l' .Data.List.List.?
  'd' .Data.List.List.? …

我想用其他方法扩展内置类HTMLElement.也许我会发疯,但我认为以下是官方成语:

interface HTMLElement {
   swapChildBefore(remove: HTMLElement, insert: HTMLElement, before: HTMLElement): void;
}

HTMLElement.prototype.swapChildBefore =
   function (remove: HTMLElement, insert: HTMLElement, before: HTMLElement): void {
      this.removeChild(remove)
      this.insertBefore(insert, before)
   }

至少,根据原型如何扩展打字稿？,这样的事情应该有效.

但是,这似乎隐藏了HTMLElement上的所有现有方法.那是因为我已经声明了一个接口,它隐藏了同名的类吗？但是这个成语似乎与Object和Array一起使用,它们也是类.

我很难说服Agda终止检查fmap下面的函数,并且在a的结构上递归地定义了类似的函数Trie.A Trie是一个trie,其域是a Type,是一个由单元,产品和固定点组成的对象级类型(我省略了副产品以保持代码最小).问题似乎与我在定义中使用的类型级替换有关Trie.(表达式const (?? ?) * ?表示将替换const (?? ?)应用于类型?.)

module Temp where

   open import Data.Unit
   open import Category.Functor
   open import Function
   open import Level
   open import Relation.Binary

   -- A context is just a snoc-list.
   data Cxt {} (A : Set ) : Set  where
      ? : Cxt A
      _??_ : Cxt A ? A ? Cxt A

   -- Context membership.
   data _?_ {} {A …

是否有与 Haskell>>运算符等效的 PureScript 标准库？

class Monad m where
...
(>>) :: m a -> m b -> m b
...

显然，定义很简单，但如果有的话，我更愿意使用库版本。