在依賴型別的函式式編程語言中，扁平化一個串列是否更容易？

當我在 haskell 中尋找一個可以平鋪任意深度嵌套串列的函式時，也就是一個遞回應用 concat 并在最后一次迭代（非嵌套串列）時停止的函式，我注意到這需要有一個更靈活的型別系統，因為隨著串列深度的變化，輸入型別也會隨之變化。事實上，有幾個 stackoverflow 問題--例如這個問題--其中的回復指出，"不可能存在一個將'看'不同深度的嵌套串列的函式"。

編輯：有些答案在 haskell 中提供了變通的方法，要么是自定義資料型別，要么是在 TypeFamilies 或 MultiParamTypeClasses 的幫助下（如下面 Noughtmare 的答案或上面帖子中 'Landei' 的答案或這個帖子中 'John L' 的答案）。 然而，這些族和類似乎也是為了在haskell中缺乏/替代從屬型別而引入的（例如，haskell wiki指出"型別族是[...]很像從屬型別"。

我現在的問題是，haskell是否真的最初不是為定義這類函式（例如扁平化不同深度的串列）而設計的，此外，一旦人們轉移到實作依賴型別的語言，這些問題是否會消失？(例如，Idris、Agda、Coq......）我對這些語言沒有經驗，所以我才會問。

例如，在Idris網站上，它說 "型別可以作為引數傳遞給函式"，因此，我想，在串列扁平化的情況下，我們也許可以簡單地將串列的型別作為引數傳遞，并以直接的方式實作所需的函式。這可能嗎？

一個后續問題也是如此。那些在haskell中解決這個問題的Families和Classes是否提供了haskell中依賴型別理論的完整實作，如果不是，有什么重要的區別？

uj5u.com熱心網友回復：

你可以在Haskell中做一個這樣的函式，在那里你不需要指定輸出型別：

{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #-}

type family FlatT a where
  FlatT [[a]] = FlatT [a]
  FlatT a = a

class Flat a where<
  flat :: a -> FlatT a
 
instance Flat [a] => Flat [[a] ] ] where>
  flat xs = flat $ concat xs

instance {-# OVERLAPPABLE #-} FlatT a ~ a => Flat a where
  平坦的x = x

main = print $ flat [["Hello"," "], ["World", "!]

仍然出現的一個問題是，你的串列中可能包含一個多型型別，而這個多型型別本身可能是一個串列。例如，你可以寫一個整數的串列：

main = print $ flat [[1, 2],[3,4, 5]]

這將給出許多關于模糊變數的錯誤。一個簡單的修復方法是給其中一個整數添加一個型別簽名。[[1,2],[3,4,5 :Int]]。這將解決所有的錯誤。

instance Num [Int] where
  fromInteger n = replicate (fromInteger n) (fromInteger n)

然后你可以這樣使用：

main = print $ [[1, 2],[3,4,5 : : [Int]]。

這將回傳：

[1,2, 2,3,3,3。 4,4,4,4, 5,5,5,5]

正如你所看到的，這多解開了一個層。所以被解開的層數取決于你在簽名中給出的型別。對我來說，這聽起來像是不可能避免型別簽名，即使在更強大的語言中。

uj5u.com熱心網友回復：

在Haskell中模仿"任意深度嵌套的串列"的一個常見方法是使用free monads。

自由單體包含在語言庫中，作為包Control.Monad.Free.

所以我們可以嘗試實作"多級串列"作為MLL型別轉換器：

import Control.Monad
import Control.Monad.Free

--多級串列:
type MLL = Free []/span>

mllJoin :: [MLL a] -> MLL a
mllJoin = Free

mllWrap :: a -> MLL a
mllWrap = return

現在的問題是：我們如何能夠扁平化這樣一個物件？ 那么，一個可能的說法是，如果Free型別建構式的漏斗引數ft是Foldable類的一個實體，那么Free ft也是。

因此，由于[]是可折疊的，我們的MLL型別轉換器也是如此。

例如，foldr的型別：

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b

可以這樣專業化：

foldr :: (a -> acct -> acct) -> acct -> MLL a -> acct

用acct作為累積器型別。

這就給出了將acct選為[a]的想法，并將cons作為foldr的功能引數。像這樣：

mllFlatten :: MLL a -> MLL a
mllFlatten xs = let fl1 = foldr（:） [] xs
                  in mllJoin (fmap mllWrap fl1)

測驗程式：

main :: IO ()
main = do
    --嘗試建立一個小型的多層次結構，如zs:。
    let xs = (mllJoin [ mllWrap 41, mllWrap 42 ] ) :: (MLL Integer)
         ys = mllJoin [ xs, mllWrap 43 ] 。
         zs = mllJoin [ mllWrap 40, ys, mllWrap 44 ]
    putStrLn $ "zs ="    (顯示 zs)
    
    --顯示zs的結構：。
    let zsImage = filter (ch -> not (elem ch "Pure Free"/span>)  (顯示 zs)
    putStrLn $ "zsImage ="/span>    zsImage

    --扁平化zs:
    let fzs = mllFlatten zs
    putStrLn $ "Flattened zs ="    （顯示fzs）。

    --顯示扁平化的zs的結構：。
    let fzsImage = filter (ch -> not (elem ch "Pure Free"/span>)  (顯示fzs)
    putStrLn $ "fzsImage ="/span>    fzsImage

測驗程式輸出：

zs = Free [Pure 40, Free [Free [Pure 41, Pure 42],Pure 43] ，Pure 44]
zsImage = [40, [[41, 42],43], 44]
Flattened zs = Free [Pure 40,Pure 41。 Pure 42,Pure 43,Pure 44]
fzsImage = [40,41, 42,43,44]

因此，看來折疊結構確實能使它變平。

uj5u.com熱心網友回復：

對于這樣的任務，Generics是一個很好的工具。 如果你的型別是一個Data的實體，你可以寫

import Data.Generics
import Control.Monad
gFind :: (MonadPlus m, Data a, Typeable b) => a -> m b
gFind = msum . map return . listify (const True)

所以，

λ> gFind [[1,2],[3,4,5] : : [Integer]
[1,2,3,4,5]
λ> gFind ((1,"b"), (2,"d","e") : : [Integer] 。
[1,2]

uj5u.com熱心網友回復：

既然你想看看如何在Coq中完成，我在這里提出一個簡單的解決方案。

From Coq Require Import Utf8 List.
Import ListNotations。

Fixpoint flatten {A}。(l : list (list A)) : list A :=
  與l匹配
  | x :: l => x    flatten l
  | [] => []
  結束。

(* Nested list type *) 
Fixpoint nlist (n : nat) (A : Type) : Type :=
  匹配n與
  | 0 => A := match n with
  | S n => list (nlist n A)
  結束。

Fixpoint nflatten {n A}. (l : nlist n A) : list A :=
  匹配n as m
  回傳 nlist m A → list A 。
  與
  | 0 => λ x, [ x ] 。
  | S n => λ l, flatten (map nflatten l)
  結束l。

Eval計算in。
nflatten (n := 2) [
  [1 ; 2 ; 3 ] 。
  [4 ; 5 ] ;
  [] ;
  [6] 。
].
(* = [1; 2; 3; 4; 5; 6]
     : list nat *)

Eval計算in。
nflatten (n := 3) [
  [[1] ; [2; 3] ] ;
  [[4 ; 5] ] 。
  [] ;
  [[6] ]。
].
(* = [1; 2; 3; 4; 5; 6]
     : list nat *)

我首先以一種天真的方式重新定義了flatten，然后我定義了一個嵌套串列的型別nlist，它帶有一個對應于深度的自然數。 我假設你希望你的所有串列都有一個恒定的深度，否則解決方案會稍微復雜一些。

那么 nflatten 將簡單地對自然數進行個案分析，以進行扁平化處理。

標籤：

上一篇：依賴包的編譯錯誤，需要一個語言擴展

下一篇：用表格提交HTMX表格