正如您所描述的，单例类型是那些只有一个值的类型（让我们忽略⊥暂时）。因此，单例类型的值具有表示该值的唯一类型。依赖类型理论 (DTT) 的关键在于类型可以依赖于值（或者，换句话说，值可以参数化类型）。允许类型依赖于类型的类型理论可以使用单例类型来让类型依赖于单例值。相反，类型类提供特设多态性，其中值可以取决于类型（与 DTT 相反，其中类型取决于值）。
Haskell 中的一项有用技术是定义一类相关的单例类型。经典的例子是自然数：
data S n = Succ n
data Z = Zero
class Nat n
instance Nat Z
instance Nat n => Nat (S n)
如果没有添加更多实例Nat, the Nat类描述单例类型，其值/类型是归纳定义的自然数。注意，Zero是唯一的居民Z但类型S Int，例如，有许多居民（它不是单例）；这Nat类限制参数S到单例类型。直观上，任何具有多个数据构造函数的数据类型都不是单例类型。
给出上面的内容，我们可以编写依赖类型的后继函数：
succ :: Nat n => n -> (S n)
succ n = Succ n
在类型签名中，类型变量n可以被视为一个值，因为Nat n约束限制n代表自然数的单例类型类。的返回类型succ then depends在此值上，其中S由值参数化n.
任何可以归纳定义的值都可以被赋予唯一的单例类型表示。
一种有用的技术是使用 GADT 用单例类型（即值）来参数化非单例类型。例如，这可以用于给出归纳定义的数据类型的形状的类型级表示。经典的例子是一个大小列表：
data List n a where
Nil :: List Z a
Cons :: Nat n => a -> List n a -> List (S n) a
这里自然数单例类型通过列表类型的长度来参数化列表类型。
从多态 lambda 演算的角度思考，succ上面有两个参数，类型n然后是类型的值参数n。因此，这里的单例类型提供了一种Π-type http://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A0-types, where succ :: Πn:Nat . n -> S(n)其中参数为succ在 Haskell 中提供了依赖的乘积参数n:Nat（作为类型参数传递），然后是参数值。
