固定长度和类型文字的列表

Question

我正在尝试为Haskell中的固定长度列表定义一个类型.当我使用标准方式将自然数编码为一元中的类型时,一切正常.但是,当我尝试在GHC的类型文字上构建所有内容时,我遇到了大量问题.

我对所需列表类型的第一次拍摄是

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

遗憾的是,它不允许使用类型编写zip函数

zip :: List n a -> List n b -> List n (a,b)

我可以通过从类型变量n中的类型变量中减去1来解决这个问题(:>):

data List (n :: Nat) a where
  Nil :: List 0 a
  (:>) :: a -> List (n-1) a -> List n a -- subtracted 1 from both n's

接下来,我尝试定义一个追加函数:

append :: List n1 a -> List n2 a -> List (n1 + n2) a
append Nil       ys = ys
append (x :> xs) ys = x :> (append xs ys)

不幸的是,GHC告诉我

Couldn't match type ‘(n1 + n2) - 1’ with ‘(n1 - 1) + n2’

((n1 + n2) - 1) ~ ((n1 - 1) + n2)由于GHC抱怨,将约束添加到签名并不能解决问题

Could not deduce ((((n1 - 1) - 1) + n2) ~ (((n1 + n2) - 1) - 1))
from the context (((n1 + n2) - 1) ~ ((n1 - 1) + n2))

现在,我显然陷入某种无限循环.

所以,我想知道是否可以使用类型文字来定义固定长度列表的类型.我是否甚至可以为这个目的监督一个图书馆？基本上,唯一的要求是我想写一些List 3 a代替的东西List (S (S (S Z))) a.

Answer 1

这不是一个真正的答案.

使用https://hackage.haskell.org/package/ghc-typelits-natnormalise-0.2,这个

{-# 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)

...编译,所以显然它是正确的.

Answer 2

类型级别数字文字还没有我们可以进行归纳的结构,内置约束求解器只能找出最简单的情况.目前最好坚持使用Peano天然产品.

但是,我们仍然可以使用文字作为语法糖.

{-# LANGUAGE
  UndecidableInstances,
  DataKinds, TypeOperators, TypeFamilies #-}

import qualified GHC.TypeLits as Lit

data Nat = Z | S Nat

type family Lit n where
    Lit 0 = Z
    Lit n = S (Lit (n Lit.- 1))

现在你可以写List (Lit 3) a而不是List (S (S (S Z))) a.