是否有具有约束类型的语言? [英] Is there a language with constrainable types?

问题描述

是否有一种类型化编程语言可以像下面两个示例那样约束类型?

Is there a typed programming language where I can constrain types like the following two examples?

1. 概率是一个浮点数，最小值为 0.0，最大值为 1.0.

1. A Probability is a floating point number with minimum value 0.0 and maximum value 1.0.

type Probability subtype of float
where
    max_value = 0.0
    min_value = 1.0

离散概率分布是一个映射，其中:键应该都是相同的类型，值都是概率，值的总和 = 1.0.

A Discrete Probability Distribution is a map, where: the keys should all be the same type, the values are all Probabilities, and the sum of the values = 1.0.

type DPD<K> subtype of map<K, Probability>
where
    sum(values) = 1.0

据我所知，Haskell 或 Agda 无法做到这一点.

As far as I understand, this is not possible with Haskell or Agda.

推荐答案

你想要的是细化类型.

可以在 Agda 中定义 Probability:Prob.agda

It's possible to define Probability in Agda: Prob.agda

概率质量函数类型，求和条件在第 264 行定义.

The probability mass function type, with sum condition is defined at line 264.

有比 Agda 更直接的细化类型的语言，例如 ATS

There are languages with more direct refinement types than in Agda, for example ATS

这篇关于是否有具有约束类型的语言?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！