固定长度和类型文字列表

问题描述

我试图在Haskell中定义一个固定长度列表的类型。当我使用标准方式将自然数编码为一元类型时，一切正常。然而，当我试图在GHC的类型文字上创建所有的东西时，我遇到了很多问题。

我第一次使用期望的列表类型是

  data列表（n :: Nat）a其中
 Nil :: List 0 a 
（：>）:: a - >列表n a  - >列表（n + 1）a 
  

不幸的是，它不允许写入类型为

  zip ::列表na  - >列表n b  - >列表n（a，b）
  

我可以通过从类型变量<$ （：>）类型中的c $ c> n ：

  data列表（n :: Nat）a其中
 Nil :: List 0 a 
（：>）:: a  - >列表（n-1）a  - >列表na  - 从n的
中减去1然后，我尝试定义一个附加函数： 
 $> p> 
 
 
  append :: List n1 a  - >列表n2 a  - > List（n1 + n2）a 
 append Nil ys = ys 
 append（x：> xs）ys = x：> （追加xs ys）
  
不幸的是，GHC告诉我
 
 
 无法将类型'（n1 + n2） -  1'与'（n1  -  1）+ n2'
  pre> 
 
 
添加约束（（n1 + n2） -  1）〜（（n1  -  1）+ n2）签名并不能解决自GHC抱怨以来的问题
 无法推论（（（（n1  -  1） -  1 （（（n1 + n2） -  1）〜（（n1  -  1）+ n2））$ b $中的
 + n2）〜（（（n1 + n2） -  1） b  
现在，我显然陷入了某种无限循环。
 
 
 
所以，我想知道是否可以使用类型文字来定义固定长度列表的类型。我是否甚至为了这个目的而监督一个图书馆？基本上，唯一的要求是我想写一些像列表3 a 而不是 List（S（S（SZ）））a 。
解决方案
 
 
这不是一个真正的答案。 
使用，this 
  { - ＃LANGUAGE GADTs＃ - } 
 { - ＃LANGUAGE TypeOperators＃ - } 
 { - ＃LANGUAGE DataKinds＃ - } 
 { - ＃LANGUAGE KindSignatures＃ - } 
 { - ＃OPTIONS_GHC -fplugin GHC.TypeLits.Normalise＃ - } 
 
导入GHC.TypeLits 
 
 data List（n :: Nat）a其中
 Nil :: List 0 a 
（：>）:: a  - >列表n a  - >列表（n + 1）a 
 
 append :: List n1 a  - >列表n2 a  - > List（n1 + n2）a 
 append Nil ys = ys 
 append（x：> xs）ys = x：> （附加xs ys）
  
 ...编译，显然是正确的。
 
 
  
I'm trying to define a type for lists of fixed length in Haskell. When I use the standard way to encode natural numbers as types in unary, everything works fine. However, when I try to build everything on GHC's type literals, I run into tons of problems.
My first shot at the desired list type was
data List (n :: Nat) a where
  Nil :: List 0 a
  (:>) :: a -> List n a -> List (n+1) a
which unfortunately didn't allow for writing a zip function with type
zip :: List n a -> List n b -> List n (a,b)
I could solve this problem by subtracting 1 from the type variable n in the type of (:>):
data List (n :: Nat) a where
  Nil :: List 0 a
  (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's
Next, I tried to define an append function:
append :: List n1 a -> List n2 a -> List (n1 + n2) a
append Nil       ys = ys
append (x :> xs) ys = x :> (append xs ys)
Unfortunately, GHC tells me
Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’
Adding the constraint ((n1 + n2) - 1) ~ ((n1 - 1) + n2) to the signature doesn't solve the problems since GHC complains
Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1))
from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2))
Now, I'm obviously caught in some kind of infinite loop.
So, I'd like to know if it is possible to define a type for lists of fixed length using type literals at all. Did I perhaps even oversee a library for precisely this purpose? Basically, the only requirement is that I want to write something like List 3 a instead of List (S (S (S Z))) a.
 解决方案 
This is not really an answer.
Using https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2 , this
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits

data List (n :: Nat) a where
  Nil :: List 0 a
  (:>) :: a -> List n a -> List (n+1) a

append :: List n1 a -> List n2 a -> List (n1 + n2) a
append Nil       ys = ys
append (x :> xs) ys = x :> (append xs ys)
... compiles, so obviously it's correct.
                        
这篇关于固定长度和类型文字列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！