Haskell中Idris的首选替代方案是什么？ [英] What is the preferred alternative to Fin from Idris in Haskell

问题描述

我想要一个可以包含值0到n的类型，其中n位于类型级别。

我正在尝试类似于：

  import GHC.TypeLits 
 import Data.Proxy 
 
 newtype FiniteNat n = FiniteNat {toInteger :: Integer} 
 
 smartConstructFiniteNat ::（KnownNat n）=>代理n  - >整数 - >也许（FiniteNat（Proxy n））
 smartConstructFiniteNat pn i 
 | 0< = i&&我< n = Just（FiniteNat i）
 |否则= Nothing 
其中n = natVal pn 
  

基本上可行，但它并不真正令人满意不知何故。是否有一个标准解决方案，甚至是一个库来实现？有很多关于依赖类型的列表长度的问题，但是我无法为此找到确切的东西。另外 - 我假设使用 GHC.TypeLits 是必要的，因为我的 n 可以取相当大的值，所以归纳定义您可以直接翻译Idris的 Fin 。

进入通常的Haskell混合类型的特性。

 数据Fin n其中
 FZ :: Fin（S n）
 FS :: Fin n  - > Fin（S n）
 
（！）:: Vec n a  - > Fin n  - > 
（x：> xs）！ FZ = x 
（x：> xs）！ （FS f）= xs！ f 
  

使用 TypeInType Fin s！

  data Finny n（f :: Fin n）其中
 FZy :: Finny（S n）FZ 
 FSy :: Finny nf  - > Finny（S n）（FS f）
  

这允许您伪装运行时的东西，例如，

  type family Fin2Nat n（f :: Fin n）其中
 Fin2Nat （S _）FZ = Z 
 Fin2Nat（S n）（FS f）= S（Fin2Nat nf）
 
  - 尽可能收紧给定翅片的上限
拧紧:: Finny nf  - > Fin（S（Fin2Nat nf））
拧紧FZy = FZ 
拧紧（FSy f）= FS（拧紧f）
  

但是，呃，有必要在值和类型级别复制所有内容，并写出所有你喜欢的变量（ n ）可以变得非常单调乏味。

---

如果您确定需要高效的 Fin ，你可以基本上做你在你的问题中做了什么：将一台机器 Int 填入 newtype code>并为其大小使用幻像类型。但是，图书馆实施者的责任在于确保 Int 符合约束！

  newtype Fin n = Fin Int 
 
  - 假构造函数
 fz :: Fin（S n）
 fz = Fin 0 
 fs :: Fin n  - > Fin（S n）
 fs（Fin n）= Fin（n + 1）
  

这个版本缺乏真正的GADT构造函数，所以你不能使用模式匹配来处理类型相等。你必须使用 unsafeCoerce 来自己做。你可以以 fold 的形式为客户提供一个类型安全的接口，但是他们必须愿意以更高阶的风格编写所有的代码， code> fold 是一种变形），一次只能查看多个图层变得更难。

   -  unsafeCoerce调用断言m〜S n 
 fold ::（forall n。rn  - > r（S n）） - > （全部nr（S n）） - > Fin m  - > rm 
 fold kz（Fin 0）= unsafeCoerce z 
 fold kz（Fin n）= unsafeCoerce $ k $ fold kz（Fin（n-1））
  

哦，你不能进行类型级计算（就像我们在上面用 Fin2Nat 做的那样）用 Fin 表示，因为类型级别 Int s不允许导入。

值得一提的是，Idris的 Fin 与上面的GADT一样低效。该文档包含以下内容注意：



使用 Fin 可能不是个好主意，对于算术运算而言，它们在运行时效率极低。

我听说过有关未来版本的Idris能够使用类型样式数据类型（比如 Fin ）将 Nat >自动擦除并将值打包到机器中整数，但据我所知，我们还没有。

I would like to have a type which can contain values 0 to n, where n lives on the type level.

I was trying something like:

import GHC.TypeLits
import Data.Proxy

newtype FiniteNat n = FiniteNat { toInteger :: Integer }

smartConstructFiniteNat :: (KnownNat n) => Proxy n -> Integer -> Maybe (FiniteNat (Proxy n))
smartConstructFiniteNat pn i 
  | 0 <= i && i < n = Just (FiniteNat i)
  | otherwise       = Nothing
  where n = natVal pn

which works basically, but it's not really satisfying somehow. Is there a "standard" solution, or even a library to achieve this? There is a lot of fuss about dependenty typed list-lengths, but I was unable to find something exactly for this. Also - I assume using GHC.TypeLits is necessary, because my n can take on rather large values, so inductive definition would probably be very slow.

解决方案

You can directly translate Idris's Fin into the usual Haskell mishmash of sort-of-dependently-typed features.

data Fin n where
    FZ :: Fin (S n)
    FS :: Fin n -> Fin (S n)

(!) :: Vec n a -> Fin n -> a
(x :> xs) ! FZ = x
(x :> xs) ! (FS f) = xs ! f

With TypeInType you can even have singleton Fins!

data Finny n (f :: Fin n) where
    FZy :: Finny (S n) FZ
    FSy :: Finny n f -> Finny (S n) (FS f)

This allows you to fake up dependent quantification over runtime stuff, eg,

type family Fin2Nat n (f :: Fin n) where
    Fin2Nat (S _) FZ = Z
    Fin2Nat (S n) (FS f) = S (Fin2Nat n f)

-- tighten the upper bound on a given Fin as far as possible
tighten :: Finny n f -> Fin (S (Fin2Nat n f))
tighten FZy = FZ
tighten (FSy f) = FS (tighten f)

but, ugh, it kinda sucks to have to duplicate everything at the value and type level, and writing out all your kind variables (n) can get pretty tedious.

---

If you're really sure you need an efficient runtime representation of Fin, you can do basically what you did in your question: stuff a machine Int into a newtype and use a phantom type for its size. But the onus is on you, the library implementer, to make sure the Int fits the bound!

newtype Fin n = Fin Int

-- fake up the constructors
fz :: Fin (S n)
fz = Fin 0
fs :: Fin n -> Fin (S n)
fs (Fin n) = Fin (n+1)

This version lacks real GADT constructors, so you can't manipulate type equalities using pattern matching. You have to do it yourself using unsafeCoerce. You can give clients a type-safe interface in the form of fold, but they have to be willing to write all their code in a higher-order style, and (since fold is a catamorphism) it becomes harder to look at more than one layer at a time.

-- the unsafeCoerce calls assert that m ~ S n
fold :: (forall n. r n -> r (S n)) -> (forall n. r (S n)) -> Fin m -> r m
fold k z (Fin 0) = unsafeCoerce z
fold k z (Fin n) = unsafeCoerce $ k $ fold k z (Fin (n-1))

Oh, and you can't do type level computation (as we did with Fin2Nat above) with this representation of Fin, because type level Ints don't permit induction.

For what it's worth, Idris's Fin is just as inefficient as the GADT one above. The docs contain the following caveat:

It's probably not a good idea to use Fin for arithmetic, and they will be exceedingly inefficient at run time.

I've heard noises about a future version of Idris being able to spot "Nat with types"-style datatypes (like Fin) and automatically erase the proofs and pack the values into machine integers, but as far as I know we're not there yet.

这篇关于Haskell中Idris的首选替代方案是什么？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！