有限制类型的语言吗？ [英] Is there a language with constrainable types?

问题描述

有没有一种类型化的编程语言，我可以像下面两个例子那样限制类型？

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

1. 概率是一个浮动
   
   

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中定义概率： 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屋！