数据类型提升为依赖性提出挑战 [英] Datatype promotion for dependently challenged

问题描述

阅读完ghc 7.4后。发布前说明和提供Haskell促销纸张，米仍然困惑你实际做什么提升类型。例如，GHC手册给出了以下关于提升的数据类型的例子：

  data Nat = Ze | Su Nat 
 
数据List a = Nil |缺点a（列表a）
 
数据Pair a b = Pair a b 
 
 data Sum a b = L a | R b 
  

它们有什么样的用途？你可以给（代码）例子吗？

解决方案

这篇论文至少有两个例子：
$ b

1。简介说：例如，我们可以确保（在编译时）所谓的红黑树真的具有红黑属性。
$ b 2.1促进数据类型讨论了长度索引的向量（即，带有编译时索引超出范围错误的向量）。

你也可以看看在这方面的早期工作，例如用于类型安全异构列表和可扩展集合的HList库。 Oleg Kiselyov 有很多相关的作品。您还可以阅读有关从属类型编程的着作。 http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf在Agda中有类型级计算的介绍性例子，但它们也可以应用于Haskell。

粗略地说，这个想法是 head 列表给出了更精确的类型。而不是

  head :: List a  - > a 
  

它是

  head :: NotEmptyList a  - > a 
  

后者头函数比fomer更安全：它永远不能应用于空列表，因为它会导致编译器错误。

您需要使用类型级计算来表达类型，如NotEmptyList。具有函数依赖关系的类类，GAGT和（索引）类型系列已经为haskell提供了弱类型级别的计算形式。您提到的工作只是在这方面进一步阐述。

请参阅 http ：//www.haskell.org/haskellwiki/Non-empty_list ，仅用于使用Haskell98类型的实现。

After reading through the ghc 7.4. pre-release notes and the Giving Haskell a Promotion paper, I'm still confused on what you actually do with promoted types. For example, the GHC manual gives the following examples on promoted datatypes:

data Nat = Ze | Su Nat

data List a = Nil | Cons a (List a)

data Pair a b = Pair a b

data Sum a b = L a | R b

What kind of uses do these have as kinds? Can you give (code) examples?

解决方案

There are at least two examples in the paper itself:

"1. Introduction" says: "for example, we might be able to ensure [at compile time] that an alleged red-black tree really has the red-black property".

"2.1 Promoting datatypes" discusses length-indexed vectors (that is, vectors with compile-time "index out of bounds" errors).

You can also take a look at earlier work in this direction, e.g. HList library for type-safe heterogenous lists and extensible collections. Oleg Kiselyov has many related works. You can also read works on programming with dependent types. http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf has introductory examples for type-level computations in Agda, but those can be applied to Haskell as well.

Roughly, the idea is that head for lists is given a more precise type. Instead of

head :: List a -> a

it is

head :: NotEmptyList a -> a

The latter head function is more typesafe than the fomer: it can never be applied to empty lists because it would cause compiler errors.

You need type-level computations to express types such as NotEmptyList. Type classes with functional dependencies, GAGTs and (indexed) type families already provide weak forms of type-level computations for haskell. The work you mentioned just elaborates further in this direction.

See http://www.haskell.org/haskellwiki/Non-empty_list for an implementation using only Haskell98 type classes.

这篇关于数据类型提升为依赖性提出挑战的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！