1

長さが制限されたリストを定義してみましょう。いえ

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

次に、このリストを共通リスト (任意の長さの入力文字列など) から初期化します。それをしてもいいですか？このような関数（またはクラス）を書くことは可能ですか?

toConsList :: [a] -> List n a

それとも、これはコンパイル時に知られている長さの構造にのみ適していますか?

4

1 に答える 1