5

どうやら、一部の GHC 拡張では、次のように、長さがエンコードされたタイプのリストを定義することが可能です。

{-# LANGUAGE GADTs, EmptyDataDecls #-}

data Z
data S a

data List l a where
  Nil  :: List Z a
  Cons :: a -> List l a -> List (S l) a

これが役立つ理由はわかりますが、実際に使用するのは難しいです。

どうすればそのようなリストを作成できますか? （プログラムにハードコーディングすることは別として。）

ターミナルから 2 つのリストを読み取り、内積を計算するプログラムを作成したいとします。実際の乗算関数を実装するのは簡単ですが、プログラムはどのようにデータを読み取るのでしょうか?

これらの手法を使用している既存のコードを教えてください。

4

3 に答える 3

3

リストの長さをハードコーディングする必要はありません。代わりに、次の型を定義できます。

data UList a where
    UList :: Nat n => List n a -> UList a

どこ

class Nat n where
    asInt :: n -> Int

instance Nat Z where
    asInt _ = 0

instance Nat n => Nat (S n) where
    asInt x = 1 + asInt (pred x)
      where
        pred = undefined :: S n -> n

そして私たちも持っています

fromList :: [a] -> UList a
fromList [] = UList Nil
fromList (x:rest) =
    case fromList rest of
        UList xs -> UList (Cons x xs)

この設定により、コンパイル時に長さが不明なリストを作成できます。caseパターンマッチを実行して存在ラッパーから型を抽出し、Natクラスを使用して型を整数に変換することで長さにアクセスできます。

コンパイル時に値がわからない型を持つことの利点は何だろうと思うかもしれません。答えは、型がどうなるか分からなくても、不変条件を適用できるということです。たとえば、次のコードは、リストの長さを変更しないことが保証されています。

mapList :: (a -> b) -> List n a -> List n b

そして、たとえば と呼ばれる型ファミリを使用した型追加がある場合、次のAddように書くことができます

concatList :: List m a -> List n a -> List (Add m n) a

これにより、2 つのリストを連結すると 2 つの長さの合計を持つ新しいリストが得られるという不変条件が適用されます。

于 2013-11-05T01:53:10.697 に答える
2

型はもちろんコンパイル時に修正され、GHC 型チェッカーのチューリング完全性を悪用して「それ自体で」それらを生成することはできないため、ハードコードする必要がほとんどありません1。ただし、これは思ったほど劇的ではありません。基本的には、長さの注釈型を 1 回記述するだけで済みます。残りは、いくつかの奇妙に見えるクラスがありますが、特定の長さについて言及することなく実行できます。

class LOL l where
  lol :: [a] -> l a

instance LOL (List Z) where
  lol _ = Nil

instance (LOL (List n)) => LOL (List (S n)) where
  lol (x:xs) = Cons a $ lol xs
  lol [] = error "Not enough elements given to make requested type length."

次に、次のようなものを使用できます

type Four = S(S(S(S Z)))

get4Vect :: Read a => IO (List Four a)
get4Vect = lol . read <$> getLine    -- For input format [1,2,3,4].

1ここで Template Haskell について議論するつもりはありません。もちろん、これはコンパイル時に何でも簡単に自動生成できます。

于 2013-11-04T20:59:13.843 に答える
2

長さのエンコーディングはコンパイル時に機能するため、タイプチェッカーは実行時にユーザー入力などから作成されたリストの長さを確認できません。アイデアは、実行時のリストを長さパラメーターを隠す存在型でラップし、リストを使用するために長さに関する証明を提供する必要があるということです。

例えば：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lists where

data Nat = Z | S Nat

data List l a where
    Nil  :: List Z a
    Cons :: a -> List n a -> List (S n) a

data DynList a where
    DynList :: List l a -> DynList a

data Refl a b where
    Refl :: Refl a a

fromList :: [a] -> DynList a
fromList []     = DynList Nil
fromList (x:xs) = cons (fromList xs) where
    cons (DynList rest) = DynList $ Cons x rest

toList :: List l a -> [a]
toList Nil = []
toList (Cons x xs) = x : toList xs

dot :: Num a => List l a -> List l a -> List l a
dot Nil Nil = Nil
dot (Cons x xs) (Cons y ys) = Cons (x*y) (dot xs ys)

haveSameLength :: List l a -> List l' b -> Maybe (Refl l l')
haveSameLength Nil Nil                 = Just Refl
haveSameLength (Cons _ xs) (Cons _ ys) = case haveSameLength xs ys of
    Just Refl -> Just Refl
    Nothing   -> Nothing
haveSameLength _ _                     = Nothing

main :: IO ()
main = do
    dlx :: DynList Double <- fmap (fromList . read) getLine
    dly :: DynList Double <- fmap (fromList . read) getLine

    case (dlx, dly) of
        (DynList xs, DynList ys) -> case haveSameLength xs ys of
            Just Refl -> print $ toList $ dot xs ys
            Nothing   -> putStrLn "list lengths do not match"

以下DynListは動的な長さのリストです (つまり、長さは実行時にしかわかりません) List。これでdot、同じ長さの 2 つのリストの内積を計算する関数ができたので、例のように stdin からリストを読み取る場合、リストが実際に同じ長さであるという証明を提供する必要があります。

ここでの「証明」はReflコンストラクターです。コンストラクターが宣言される方法は、型の値を提供Refl a bできる場合、同じ型aでなければならないことを意味します。bしたがって、 を使用しhasSameLengthて、生成された値の型とパターンの一致を検証し、Refl型チェッカーに十分な情報を提供してdot、2 つの実行時リストで呼び出すことができるようにします。

つまり、これが本質的に意味することは、コードをコンパイルするために、コンパイル時に不明なリストの長さをタイプチェッカーが手動で検証することを強制するということです。

于 2013-11-05T06:58:41.980 に答える