因为这样做各种依赖性类型形式化技术的调查的一部分，我已经跨越纸主张（有一个居民类型）使用单种作为支持依赖性类型编程的方式运行。
Acording此源，在Haskell，有介乎运行时的值的分离和编译时可以使用单种的情况下，由于感应类型/值同构被模糊的类型。
我的问题是：如何单从类型类型类或转引自/物化结构在这方面有什么不同？
我还特别欣赏相对于该类型的理论重要性一些直观的解释/使用单类型和的程度优点，他们可以在一般的模拟依赖性的类型。
Answer 1:
当你形容，单类型是那些只有一个值（让我们忽略⊥的时刻）。 因此，一个单类型的值具有表示的值的唯一类型。 依赖型理论（DTT）的关键是，类型可以取决于值（或者，所述另一方式，值可参数化的类型）。 A型理论，让类型取决于类型可以使用单种让类型取决于单值。 与此相反，类型类提供特设多态 ，其中值可以（倒过来，以DTT其中类型取决于值）依赖于类型。
Haskell中有用的技术是定义一个类相关的单类型的。 典型的例子是自然数的：
data S n = Succ n
data Z = Zero
class Nat n
instance Nat Z
instance Nat n => Nat (S n)
提供了进一步的实例不被添加到Nat ，所述Nat类描述单类型，它们的值/类型归纳定义自然数。 需要注意的是， Zero是唯一的居民Z但类型S Int ，例如，有许多居民（它不是一个单）; 的Nat类限制的参数S到单类型。 直观地，一个以上的数据构造的任何数据类型不是一个单型。
给上面，我们可以写出依赖性类型的后继函数：
succ :: Nat n => n -> (S n)
succ n = Succ n
在类型签名，类型变量n可以由于被看作是一个值Nat n约束限制n到类代表自然数单类型的。 所述的返回类型succ然后取决于该值，其中S由值参数化n 。
可以感应地定义的任何值可被赋予一个唯一的单类型的表示。
一个有用的技术是使用GADTs到参数化非单类型的单型（即，具有值）。 这可以用来，例如，以得到感应定义的数据类型的形状的类型级表示。 典型的例子是一个大小列表：
data List n a where
Nil :: List Z a
Cons :: Nat n => a -> List n a -> List (S n) a
在这里，自然数单参数化类型列表式由它的长度。
在多晶型演算的思维， succ上面有两个参数，类型n然后类型的值参数n 。 因此，单类型在这里提供了一种Π型 ，其中succ :: Πn:Nat . n -> S(n) succ :: Πn:Nat . n -> S(n)其中的参数succ在Haskell既提供从属产品参数n:Nat （作为类型参数传递），然后将参数值。
文章来源: Singleton types in Haskell
