9

そのため、新しい拡張機能を利用できるタスクを最終的に見つけましたDataKinds(ghc 7.4.1 を使用)。これがVec私が使用しているものです：

data Nat = Z | S Nat deriving (Eq, Show)

data Vec :: Nat -> * -> * where
    Nil :: Vec Z a
    Cons :: a -> Vec n a -> Vec (S n) a

さて、便宜上、実装したいと思いましたfromList。基本的に単純な再帰/折り畳みでは問題ありませんが、正しい型を与える方法がわかりません。参考までに、これは Agda のバージョンです。

fromList : ∀ {a} {A : Set a} → (xs : List A) → Vec A (List.length xs)

ここで見た構文を使用した私のHaskellアプローチ：

fromList :: (ls :: [a]) -> Vec (length ls) a
fromList [] = Nil 
fromList (x:xs) = Cons x (fromList xs)

これは私にparse error on input 'a'. 私が見つけた構文は正しいですか、それとも変更されていますか? また、リンクのコードにあるいくつかの拡張機能を追加しましたが、どちらも役に立ちませんでした (現在私は持っていますGADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies, UndecidableInstances)。

私の他の疑いは、多態型をバインドできないということでしたが、これに対する私のテスト:

bla :: (n :: Nat) -> a -> Vec (S n) a
bla = undefined

も失敗しましたKind mis-match Expected kind 'ArgKind', but 'n' has kind 'Nat'（それが何を意味するのか本当にわかりません）。

の作業バージョンを手伝ってくれたりfromList、他の問題を明確にしたりできますか? 残念ながら、DataKindsまだ十分に文書化されておらず、それを使用するすべての人が深い型理論の知識を持っていると想定しているようです。

4

3 に答える 3

10

Haskell は、Agda とは異なり、従属型を持たないため、必要なことを正確に実行する方法はありません。Haskell は実行時とコンパイル時のフェーズの区別を強制するため、型を値でパラメーター化することはできません。概念的に動作する方法DataKindsは、実際には非常に単純です。データ型は種類 (型の型) に昇格され、データ コンストラクターは型に昇格されます。 

 fromList :: (ls :: [a]) -> Vec (length ls) a

にはいくつかの問題があります:(ls :: [a])本当に意味がありません (少なくとも、昇格によって依存型を偽造しているだけの場合)、length型関数ではなく型変数です。言いたいことは

 fromList :: [a] -> Vec ??? a

は???リストの長さです。問題は、コンパイル時にリストの長さを取得する方法がないことです...

 fromList :: [a] -> Vec len a

しかし、これは間違っていfromListます。任意の長さのリストを返すことができるからです。代わりに私たちが言いたいのは

 fromList :: exists len. [a] -> Vec len a

しかし、Haskell はこれをサポートしていません。その代わり

 data VecAnyLength a where
     VecAnyLength :: Vec len a -> VecAnyLength a 

 cons a (VecAnyLength v) = VecAnyLength (Cons a v)

 fromList :: [a] -> VecAnyLength a
 fromList []     = VecAnyLength Nil
 fromList (x:xs) = cons x (fromList xs)

実際にVecAnyLengthby パターン マッチングを使用して、(ローカルに) 疑似依存型の値を取得できます。

同様に、

bla :: (n :: Nat) -> a -> Vec (S n) a

Haskell 関数は kind の引数しかとれないため、 は機能しません*。代わりに、試してみてください

data HNat :: Nat -> * where
   Zero :: HNat Z
   Succ :: HNat n -> HNat (S n)

bla :: HNat n -> a -> Ven (S n) a

これは定義可能です

bla Zero a     = Cons a Nil
bla (Succ n) a = Cons a (bla n a)
于 2012-06-28T11:50:31.653 に答える
4

You can use some typeclass magic here (see HList for more):

{-# LANGUAGE GADTs, KindSignatures, DataKinds, FlexibleInstances
  , NoMonomorphismRestriction, FlexibleContexts #-}

data Nat = Z | S Nat deriving (Eq, Show)

data Vec :: Nat -> * -> * where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

instance Show (Vec Z a) where
  show Nil = "."

instance (Show a, Show (Vec m a)) => Show (Vec (S m) a) where
  show (Cons x xs) = show x ++ " " ++ show xs

class FromList m where
  fromList :: [a] -> Vec m a

instance FromList Z where
  fromList [] = Nil

instance FromList n => FromList (S n) where
  fromList (x:xs) = Cons x $ fromList xs

t5 = fromList [1, 2, 3, 4, 5]

but this not realy solve the problem:

> :t t5
t5 :: (Num a, FromList m) => Vec m a

Lists are formed at runtime, their length is not known at compile time, so the compiler can't infer the type for t5, it must be specified explicitly:

*Main> t5

<interactive>:99:1:
    Ambiguous type variable `m0' in the constraint:
      (FromList m0) arising from a use of `t5'
    Probable fix: add a type signature that fixes these type variable(s)
    In the expression: t5
    In an equation for `it': it = t5
*Main> t5 :: Vec 'Z Int
*** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList

*Main> t5 :: Vec ('S ('S ('S 'Z))) Int
1 2 3 *** Exception: /tmp/d.hs:20:3-19: Non-exhaustive patterns in function fromList

*Main> t5 :: Vec ('S ('S ('S ('S ('S 'Z))))) Int
1 2 3 4 5 .
*Main> t5 :: Vec ('S ('S ('S ('S ('S ('S ('S 'Z))))))) Int
1 2 3 4 5 *** Exception: /tmp/d.hs:23:3-40: Non-exhaustive patterns in function fromList

Languages ​​with dependent types have maps from terms to types, types can be formed dynamically at runtime too, so this problem does not exist.

于 2012-06-28T13:09:23.493 に答える