总(功能)语言是可以显示所有内容终止的语言.显然,有很多地方我不想要这个 - 抛出异常有时很方便,Web服务器不应该终止等等.但有时候,我希望进行本地整体检查以启用某些优化.例如,如果我有一个可证明的全部功能

commutativity :: forall (n :: Nat) (m :: Nat). n + m :~: m + n
commutativity = ...

然后,由于:~:只有一个居民(Refl),GHC可以优化

gcastWith (commutativity @n @m) someExpression
  ==>
someExpression

我的可交换性证明从O(n)运行时成本到免费.那么,现在我的问题:

为Haskell制作总体检查器有哪些微妙的困难？

显然,这样的检查是保守的,所以每当GHC不确定某些东西是完全的(或者是懒得检查)时,它可能会认为它不是......在我看来,拼凑一个不是 - 可能并不太难如此智能的检查器仍然非常有用(至少它应该是直截了当地消除我所有的算术证明).然而,我似乎无法找到任何努力在GHC中构建这样的东西,所以显然我错过了一些非常大的限制.来吧,粉碎我的梦想.:)

相关但不是最近的:2005年尼尔米切尔解散Haskell.

我试图弄清楚我需要什么样的HTML/CSS才能获得某种破坏行为,具体取决于可用的空间大小.基本上,我希望有一长串文本在某些地方自动中断,而且只有一个时间,当它不再有空间时.

例1:

• 整个文本行有足够的水平空间:

  

• 整条线没有足够的水平空间(但即使前两个项目有空间,一切都在自己的线上)

示例2:这与前一个示例相同,但它表明我也希望能够以嵌套方式使用它:

• 整个文本行有足够的水平空间:

  

• 整条线路没有足够的水平空间,因此每个单元都会进入自己的线路

  

• 第二个单元没有足够的水平空间

  

我正在寻找一种只使用HTML和CSS(或者只是非常轻松地使用JavaScript)的解决方案,因为我的预期用例是在自动生成的HTML文档页面中大量使用它.

我遇到喜欢的例子,这些,但我不知道我看到如何使这项工作子项(以及如何使这项工作不分配一个固定大小的每个细胞-我想小区大小来确定按其内容).

Clarfiying编辑

只是特别强调一个被忽视的问题的关键部分.我从不想发现自己处于一行中有两个项目而下一行有第三个项目的状态.这三个项目应该直接从一条线上的所有线条直接到另一条线条.

昨天的一个问题有一个定义HList(来自HList包)使用数据系列.基本上:

data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)

pattern HCons x xs = HCons1 (x, xs)

而不是通常的(IMO更优雅和直观)GADT定义

data HList (l :: [*]) where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

这是因为数据系列版本允许我们强制(我们只能强制执行HList (x ': xs)案例,因为它是a newtype instance,但这就足够了),而GADT只推断一个名义角色l(从而阻止任何强制).(我对上述问题的回答有一个具体的例子.)

HList在这个为期两年的问题中,讨论了GADT角色系统的失败问题.基本上,GHC会自动将任何"类GADT"类型变量标记为名义变量. …

既然我们有内射类型族,那么在类型族中使用数据族是否有剩余的用例？

回顾过去几年关于数据系列的StackOverflow问题,几年前就有这个问题讨论类型族和数据族之间的区别,以及关于数据族用例的答案.两者都说数据家族的注入力是他们最大的优势.

看一下关于数据族的文档,我看到有理由不重写使用内射类型族的数据族的所有用法.

例如,假设我有一个数据系列(我已经合并了一些来自文档的示例,试图挤压数据系列的所有功能)

data family G a b
data instance G Int Bool = G11 Int | G12 Bool deriving (Eq)
newtype instance G () a = G21 a
data instance G [a] b where
   G31 :: c -> G [Int] b
   G32 :: G [a] Bool

我不妨把它改写成

type family G a b = g | g -> a b
type instance G Int Bool = G_Int_Bool
type instance …

众所周知的事实(>>=)可以使用而实现fmap,join并且join可以使用实现>>=.是否有任何理由我们没有Monad使用join包含和使用以下默认定义来定义类？

join x  = x >>= id
x >>= f = join $ f <$> x

这将允许最小定义包括just (>>=)或join,而不是强制(>>=).考虑到类别理论倾向于支持,可能会有点帮助join.

反对修改类的常见理由是我们打破了向后兼容性.但是,在这种情况下,这不会发生 - 我们只增加了定义Monad使用的可能性join.

是否可以使用FFI或其他技巧从Haskell(在GHC上)调用Clojure函数？在这里,我有兴趣保持在GHC的范围内(即,不使用弗雷格).我也有兴趣将中心程序保存在Haskell中(意味着应该从Haskell调用Clojure函数,反之亦然).

这该怎么做？

我发现Haskell Data.Vector.*错过了C++ std::vector::push_back的功能.有grow/ unsafeGrow,但它们似乎有O(n)复杂性.

有没有办法在O(1)元素的摊销时间内增长向量？

所述DataKinds扩展促进"值"(即构造函数)分为不同的类型.例如,True并False成为不同类型的种类Bool.

我想做的是相反的,即将类型降级为值.具有此签名的函数可以正常:

demote :: Proxy (a :: t) -> t

我实际上可以做到这一点,例如Bool:

class DemoteBool (a :: Bool) where
  demoteBool :: Proxy (a :: Bool) -> Bool

instance DemoteBool True where
  demoteBool _ = True

instance DemoteBool False where
  demoteBool _ = False

但是,我必须为我想要降级到它的价值的任何类型编写实例.有没有更好的方法来做这个不涉及太多的样板？

这可能听起来有点荒谬,但GHC无法编制包含培根,羊角面包,黄瓜和土豆的字符串:

main = putStrLn "      "

我意识到我可以轻松写作

main = putStrLn "\x1F953  \x1F950  \x1F952  \x1F954"

同样的效果,但我一直认为GHC会在其来源中接受任何unicode.那么:GHC在源文件中接受的unicode字符的实际限制是什么？

顺便说一句:我意识到支持这类事情对于GHC词法分析器来说是地狱(实际上我在为我写的词法分析器编写测试用例时遇到了上述问题),但我仍然有点失望.

我并不认为Haskell正在处理消息传递之类的事情,但是这些结果(我正在查看比其他任何事情好4-5倍的Linux)让我对此提出质疑.一些讨论让我进入了Cloud Haskell,它实际上似乎是一个有用的编写良好的分布式系统相关库的集合(对于这个和静态指针的工作,对Well-Typed和Tweag I/O的严重赞誉).

我对Actors和消息传递的体验源于我对Akka的使用.我正在尝试理解Cloud Haskell能够做什么来确定我是否希望将其用于可扩展性,效率和可靠性非常重要的潜在项目.所以:

• 它是否支持演员？如果没有,那等价的抽象是什么？它如何处理消息传递/丢失消息？
• 与Akka相比,它的规模如何？内存使用和延迟大致有多好/多差？
• 它如何扩展到多个节点(如缩放到多个节点有多简单)？
• 它是如何容错的？

我意识到这个问题有点宽泛,但我认为如果有人对Cloud Haskell有一些经验,他们可能会很容易地解决所有这些问题 - 这个问题对于那些搜索一般信息的人来说会更有用关于Cloud Haskell与Akka的未来.