小编Bol*_*eth的帖子

最好的方法是获取函数的表示(如果它可以以某种方式恢复).出于效率原因,优选二进制序列化.

我认为有一种方法可以在Clean中实现,因为实现iTask是不可能的,因为当服务器再次运行时,依赖于任务(以及其他功能)可以保存并继续.

这对于分布式haskell计算必不可少.

我不打算在运行时解析haskell代码,如下所述:Haskell中的函数序列化.我还需要序列化而不仅仅是反序列化.

我在Haskell中有一个非终止表达式.我想调试并检查它没有终止的原因.我学到的一种技术是在GHCi中使用以下内容:

:set -fbreak-on-exception
:trace nonterminating_expression
^C
:hist 50

所以我可以看到在无限计算中运行的指令.问题是我想继续计算:step,忽略中断.我能这样做吗？

用于调试非终止计算的任何其他解决方案？(历史大于50条记录或其他实践来帮助完成任务.)

我需要在* -> *类型之间建立排序,基于一种类型的每个成员可以由另一种类型表示.这是同态.

问题是我可以定义!<=!关系的传递性,但类型检查器无法弄清楚它.它也很模糊,Identity !<=! Maybe可以从Identity !<=! Maybe或得出Identity !<=! Identity !<=! Maybe......每个派生都有一个不同的(但等价的)定义repr.

所以我正在寻找其他方式来创造一种反思性和传递性的关系.

{-# LANGUAGE ScopedTypeVariables, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, AllowAmbiguousTypes, OverlappingInstances #-}

import Control.Monad.Identity
import Data.Maybe

class x !<=! y where
  repr :: x a -> y a

instance x !<=! x where
  repr = id

instance Identity !<=! Maybe where
  repr = return . runIdentity

instance Maybe !<=! [] where
  repr = maybeToList

instance (x !<=! …

当使用类型族的数据种类时,我发现了一个有趣的情况.

编译器的错误消息是No instance for (C (ID ())) arising from a use of W.它表明类型族应用程序即使在饱和状态下也未得到充分评估.:kind! ID ()评估为(),因此C ()应根据实例使用.

{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances, FlexibleContexts #-}

type family ID t where
  ID t = t

class C t where
instance C () where

data W where
  W :: C (AppID t) => P t -> W

type family AppID t where
  AppID t = (ConstID t) ()

type family ConstID t where
  ConstID t = …

我正在考虑功能语言的标准库(或前奏).

如果我有Ord实例n,那么实现它是微不足道的abs:

abs n = if n > 0 then n else (-n)

在向量空间的情况下,向量的绝对值(长度)非常重要.但是类型不匹配,因为向量的绝对值不是向量:它是实数.

将abs(或signum)作为Num类型类的一部分背后的设计原理是什么？

我正在使用嵌入在Haskell中的语言.我的语言可以作为源代码打印出来,所以我创建了一个Compile类,并为每个可以打印出来的程序元素创建了一个类实例.这样我就可以合成地转储我的代码.在考虑模式的概念之前,这很好.

每种语言都可以使用两种模式(作为类的实例实现Mode).在简单模式下一切正常.在命名模式下,许多程序元素可以用字符串替换.(它像宏定义一样工作.)

我想保持所有表示类型安全.因此,不能混合不同语言或不同模式的程序元素.

所以问题是:如何在不管模式的情况下转储语言？

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
class Compile a where
  comp :: a -> String

-- common elements in all languages
data ElemA l m = ElemA (ElemB l m)
data ElemB l m = ElemB

class Lang l where
  -- language-specific elements
  data Instructions l :: * -> *

-- common modes for all languages
class Mode l m where
  type MElemA l m :: *
  type MElemB l m :: …

我对依赖类型语言感兴趣.有限数字对我来说似乎非常有用.例如,安全地索引固定大小的数组.但这个定义对我来说并不清楚.

Idris中有限数字的数据类型如下:(并且在Agda中可能类似)

data FiniteNum : Natural -> Type where
  FZero : FiniteNum (Succ k)
  FSucc : FiniteNum k -> FiniteNum (Succ k)

它似乎工作:

exampleFN : FiniteNum (Succ (Succ Zero))
exampleFN = FSucc FZero -- typechecks
-- exampleFN = FSucc (FSucc FZero)  -- won't typecheck

但这是如何工作的？k是什么意思？为什么类型检查器接受第一个实现并拒绝第二个？

我很感兴趣,因为我想检查Prelude中内置函数的定义.

我搜索了它,但只在〜/ .cabal/share/idris中找到了预编译的文件...

我需要给失败消息以秒为单位的给定位置。

在给出意外错误消息之前，我尝试通过设置位置来进行操作，但是它没有用：

runParser ( do pos0 <- getPosition
               id <- many1 alphaNum
               if (id == reverse id) then return id
                                     else setPosition pos0 >> unexpected id
               eof )
          () "" "abccbb"

回馈

Left (line 1, column 7):
unexpected end of input
expecting letter or digit

正确的答案是：

unexpected abccbb
expecting letter or digit

通过省略可以生产（位置错误） setPosition pos0 >>代码。

我的解决方法是进行解析，将正确和实际的错误位置保存在parsec的用户状态下，并更正错误位置，但是我想要一个更好的解决方案。

正如AndrewC所要求的那样，它是向用户提供带有更多信息的错误消息的一部分。例如，在某些地方，我们需要特殊的标识符，但是如果在解析器中对其进行编码，parsec将给出错误消息，例如“期望的ag，得到一个r，位置在标识符的中间”。正确的消息应该是“标识符应采用特殊格式，但位置为'abccbb'，位置在标识符之前”。如果有更好的方法可以发出这样的错误消息，那将是对我们问题的正确答案。但是我也很好奇为什么parsec会那样，为什么我不能引发自定义错误消息，指向我想要的位置。

测试声明不是类型正确的最佳方法是什么？使用GADT,弄清楚构造函数应用程序是否正确并非易事.如果正在编写类型安全的构造库,则很自然地确保无法创建非法构造.因此,作为测试套件的一部分,我想确保类型检查器拒绝某些示例非法构造.

例如,请参阅尺寸检查的Vector表示.它比我想要决定的典型问题简单得多,但它是检查测试方法的一个很好的例子.

data Vector n t where
  EmptyVec :: Vector 0 t
  ConsVec  :: t -> Vector n t -> Vector (n+1) t

// TODO: test that it does not typecheck
illegalVec = ConsVec 'c' (ConsVec "b" EmptyVec)

我试图证明关于整数的可分性问题.首先,我试图证明可分性是反思性的.

?-refl : ?{n} ? n ? n

因为我根据减法定义了可分性......

data _?_ : ? ? ? ? Set where
  0?d : ?{d} ? zero ? d
  n-d?d : ?{n d} ? (n - d) ? d ? n ? d

......如果我使用以下事实似乎很容易n-n=0:

?-refl {n} with n-n?0 n 
... | refl = n-d?d 0?d

但是Agda拒绝在refl上进行模式匹配.即使没有其他可能的正常形式n-n=0 n.我用其他功能证明了这一点.我只需要使用这个事实n-n=0.

C:\Users\ebolnme\Desktop\agda\Integers.agda:118,7-11
n + neg n != zero of type ?
when checking that the pattern refl has type n + neg …