Iva*_*nin 25 haskell agda dependent-type
是否有类型化的编程语言,我可以约束类型,如下面的两个例子？
概率是一个浮点数,最小值为0.0,最大值为1.0.
type Probability subtype of float
where
max_value = 0.0
min_value = 1.0
离散概率分布是一个映射,其中:键应该都是相同的类型,值都是概率,值的总和= 1.0.
type DPD<K> subtype of map<K, Probability>
where
sum(values) = 1.0
据我所知,Haskell或Agda无法做到这一点.
Tik*_*vis 26
您可以在Haskell中使用Liquid Haskell执行此操作,该Haskell使用细化类型扩展Haskell .谓词是在编译时的SMT求解器管理,这意味着证明是完全自动的,但你可以使用逻辑由SMT求解器处理什么限制.(令人高兴的是,现代SMT求解器具有相当的通用性!)
一个问题是我不认为Liquid Haskell目前支持浮点数.如果不是这样,虽然,它应该是可能的纠正,因为是浮点数SMT求解器理论.您还可以假装浮点数实际上是合理的(甚至可以Rational在Haskell中使用!).考虑到这一点,您的第一个类型可能如下所示:
{p : Float | p >= 0 && p <= 1}
你的第二种类型编码会有点困难,特别是因为地图是一种难以推理的抽象类型.如果您使用了对列表而不是地图,您可以编写一个"度量",如下所示:
measure total :: [(a, Float)] -> Float
total [] = 0
total ((_, p):ps) = p + probDist ps
(您可能需要换[]一个newtype了.)
现在,您可以total在细化中使用约束列表:
{dist: [(a, Float)] | total dist == 1}
Liquid Haskell的巧妙之处在于,所有的推理都是在编译时自动完成的,以换取使用有限约束的逻辑.(类似total的测量也非常局限于它们的编写方式 - 它是Haskell的一小部分,其规则类似于"每个构造函数只有一个案例".)这意味着这种类型的细化类型功能不强,但比完全更容易使用 - 依赖类型,使它们更实用.
Perl6有一个"类型子集"的概念,可以添加任意条件来创建"子类型".
特别针对您的问题:
subset Probability of Real where 0 .. 1;
和
role DPD[::T] {
has Map[T, Probability] $.map
where [+](.values) == 1; # calls `.values` on Map
}
(注意:在当前实现中,"where"部分在运行时被检查,但是因为"真实类型"在编译时被检查(包括你的类),并且因为is purestd中有纯注释()(这主要是perl6)(那些也是像*等等的运营商),它只是努力的事情(它应该不会更多).
更普遍:
# (%% is the "divisible by", which we can negate, becoming "!%%")
subset Even of Int where * %% 2; # * creates a closure around its expression
subset Odd of Int where -> $n { $n !%% 2 } # using a real "closure" ("pointy block")
然后,您可以检查数字是否与智能匹配运算符匹配~~:
say 4 ~~ Even; # True
say 4 ~~ Odd; # False
say 5 ~~ Odd; # True
并且,由于multi subs(或多种方式,真正的 - 多种方法或其他方法),我们可以基于以下方式进行调度:
multi say-parity(Odd $n) { say "Number $n is odd" }
multi say-parity(Even) { say "This number is even" } # we don't name the argument, we just put its type
#Also, the last semicolon in a block is optional
Nimrod是一种支持这一概念的新语言.它们被称为子范围.这是一个例子.您可以了解更多关于语言这里链接
type
TSubrange = range[0..5]