배열 및 타입 클래스 리프트 (종속 타입?)

Question

하자가 입력 b가 Monoid의 인스턴스이며, 고정 지수 i가 입력 클래스 Ix 속하는으로 (v1,v2) :: (i,i)의 범위에서 I는 해당 데이터를 정의 할 수 있음을 말한다. 배열 유형도 Monoid가됩니다. 어떻게 할 수 있습니까? 여기서 mempty은 배열이 mappend - operation 구성 요소와 동일해야하므로 항목이 mempty::b이고 배열이 mappend 인 배열이어야합니다.

은 (예를 들어 i=(Int,Int) 경우 유형 Data.Array i b는 차원 (2) 다른 크기 (인덱스의 다른 범위)로 matricies 모든이. 만 고정 된 크기와 같은 Monoid -declaration 말이으로 나타냅니다. 사실, 나는에 관심이 있어요 Monoids 대신 Vector-space 케이스가 있지만 Monoid는 이미 어려움을 보여줍니다. 종속 유형에 대한 모호한 아이디어가 있지만이 유형의 유일한 하위 집합에 해당하는 개별 유형의 프로토 타입 예제 인 것 같습니다. 하나 개의 매개 변수가 유용 할 것이다)

는

Answer 1

일반적인 방법은 다음과 같이 더 입력 된 하나에하지-매우 형식의 표현을 포장하는 것입니다.

차원의 크기와 m의리스트 (또한 촉진 및 팬텀)이리스트의 길이 - 여기 ns

data Nat = Z | S Nat 
newtype Vec (n :: Nat) a = Vec [a] 
newtype Sized m (ns :: [Nat]) a = Sized { getArray :: Array (Vec m Int) a } 

은 (Motivation behind Phantom Types? 참조) 값이 촉진 (Giving Haskell a Promotion 참조) 팬텀이다. 따라서 Sized 래퍼 아래의 모든 배열은 차원을 나타내는 ns이있는 다차원 행렬로 간주됩니다. Monoid 예는 다음과 같습니다 SingI 물건이 singletons 라이브러리입니다

instance (SingI m, SingI ns, Monoid a) => Monoid (Sized m ns a) where 
    mempty      = listSized $ repeat mempty 
    Sized as `mappend` Sized bs = listSized $ zipWith mappend (elems as) (elems bs) 

있다. 싱글 톤을 사용하면 값을 타입 레벨로 들여 올 수 있으므로 종속 타입을 다소 에뮬레이션 할 수 있으며 SingI은 fromSing 함수를 통해 값 레벨에서 해제 된 값을 다시 가져올 수 있습니다. listSized은 본질적으로 listArray이지만 정적으로 알려진 크기를 가진 배열의 경우 해당 범위에있는 모든 SingI이 필요합니다.

toInt :: Nat -> Int 
toInt = go 0 where 
    go !a Z = a 
    go a (S n) = go (1 + a) n 

vecBounds :: forall m (ns :: [Nat]). (SingI m) => Sing ns -> (Vec m Int, Vec m Int) 
vecBounds singNs = (Vec $ replicate m 0, Vec ns') where 
    m = toInt $ fromSing (sing :: Sing m) 
    ns' = map (pred . toInt) $ fromSing singNs 

listSized :: forall m (ns :: [Nat]) a. (SingI m, SingI ns) => [a] -> Sized m ns a 
listSized = Sized . listArray (vecBounds (sing :: Sing ns)) 

vecBounds 치수의 크기가 주어진 승진 목록에 대한 경계를 계산 : 다음의 정의입니다. 튜플은 첫 번째 구성 요소가 항상 하위 참조 인덱스 인 [0,0..0] (크기가 0보다 많은 경우, 즉 m)을 반환합니다. 두 번째 구성 요소가 가장 큰 색인이므로 예를 들어 [2, 1, 3] (예 : [S (S Z), S Z, S (S (S Z))]으로 표시)의 크기 목록이있는 경우 최대 색인은 [1, 0, 2]입니다.

그것은 단지 the product instances의 직접적인 일반화되는 Vec n a에 대한 Ix 인스턴스를 제공하기 위해 남아 :

instance Ix a => Ix (Vec n a) where 
    range (Vec ns, Vec ms)   = map Vec . sequence $ zipWith (curry range) ns ms 
    index (Vec ns, Vec ms) (Vec ps) = foldr (\(i, r) a -> i + r * a) 0 $ 
    zipWith3 (\n m p -> (index (n, m) p, rangeSize (n, m))) ns ms ps 
    inRange (Vec ns, Vec ms) (Vec ps) = and $ zipWith3 (curry inRange) ns ms ps 

는 그리고 우리는 몇 가지 테스트를 작성할 수 있습니다

이

type M = S (S (S Z)) 
type Ns = [S (S Z), S Z, S (S (S Z))] 

arr1 :: Sized M Ns (Sum Int) 
arr1 = listSized $ map Sum [5,3,6,7,1,4] 

arr2 :: Sized M Ns (Sum Int) 
arr2 = listSized $ map Sum [8,2,9,7,3,6] 

main = mapM_ (print . getArray) $ [arr1, arr2, arr1 `mappend` arr2 `mappend` mempty] 

이

array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 5}),(Vec [0,0,1],Sum {getSum = 6}),(Vec [0,0,2],Sum {getSum = 1}),(Vec [1,0,0],Sum {getSum = 3}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 4})] 
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 8}),(Vec [0,0,1],Sum {getSum = 9}),(Vec [0,0,2],Sum {getSum = 3}),(Vec [1,0,0],Sum {getSum = 2}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 6})] 
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 13}),(Vec [0,0,1],Sum {getSum = 15}),(Vec [0,0,2],Sum {getSum = 4}),(Vec [1,0,0],Sum {getSum = 5}),(Vec [1,0,1],Sum {getSum = 14}),(Vec [1,0,2],Sum {getSum = 10})] 

를 인쇄를

즉 요소는 필요에 따라 점으로 합쳐졌습니다.

type Ns = [S (S Z), S Z, S (S (S Z))] 
type Ns' = [S (S (S Z)), S Z, S (S Z)] 

arr1 :: Sized M Ns (Sum Int) 
arr1 = listSized $ map Sum [5,3,6,7,1,4] 

arr2 :: Sized M Ns' (Sum Int) 
arr2 = listSized $ map Sum [8,2,9,7,3,6] 

main = print . getArray $ arr1 `mappend` arr2 

-- Couldn't match type 'S 'Z with 'Z … 
-- Expected type: Sized M Ns (Sum Int) 
-- Actual type: Sized M Ns' (Sum Int) 
-- In the second argument of `mappend', namely `arr2' 
-- In the first argument of `mappend', namely `arr1 `mappend` arr2' 

Full code : 당신이 실수로 다른 차원으로 배열을 요약하려고하면, 당신은 유형의 오류가 발생합니다.

Answer 2

@ user3237465 's는 Array에 정적 크기 정보를 첨부하는 방법에 대한 질문에 대한 완전하고 직접적인 답변입니다. 그러나 당신이 의존형에 대해 아주 새로운 것을 언급 했으므로, 주제에 대한 더 나은 소개로 작용할 수 있다고 생각되는 매트릭스 추가의 간단한 예제를 제공하고자했습니다. the Hasochism paper에 다음 중 많은 부분을 찾을 수 있습니다 (더 설명 됨).

평상시와 같이 자연수가 있으며 GHC는 자동으로 유형 수준으로 올라갑니다. 다음 data 선언은 우리는 또한 종류Nat 두 유형을 생성자 Z 및 S를 얻을 수, 유형 Nat 두 개의 값 생성자 Z 및 S을 정의 않습니다뿐만 아니라.

data Nat = Z | S Nat 

type One = S Z 
type Two = S (S Z) 
type Three = S (S (S Z)) 

나는 작전 길이의 정적 지식을 가진 연결리스트 인 관습 벡터 GADT를 정의하는거야.

infixr 5 :> 
data Vec n a where 
    VNil :: Vec Z a 
    (:>) :: a -> Vec n a -> Vec (S n) a 
deriving instance Show a => Show (Vec n a) 

instance Functor (Vec n) where 
    fmap f VNil = VNil 
    fmap f (x :> xs) = f x :> fmap f xs 

다음은 몇 가지 예시적인 벡터입니다.

v1 :: Vec Two String 
v1 = "foo" :> "bar" :> VNil 
v2 :: Vec Two String 
v2 = "baz" :> "quux" :> VNil 
v3 :: Vec One String 
v3 = "nabble" :> VNil 

유형 수준 숫자의 런타임 분석을 수행해야합니다. 예를 들어, 주어진 요소 인 n 번을 반복하는 함수 vreplicate :: n -> a -> Vec n a을 작성하고 싶습니다. vreplicate은 실행시 을 알고 있어야합니다. 얼마나 많은 복사본을 만들어야합니다! 그러나 Haskell은 런타임 값과 컴파일 타임 타입을 분리하기 때문에 위의 타입 서명은 유효하지 않습니다. 종류가 Nat 인 유형은 런타임에 전달할 수 없습니다. 싱글 톤 값을 입력하십시오.

data Natty n where 
    Zy :: Natty Z 
    Sy :: Natty n -> Natty (S n) 

는 주어진 (잘 정의) 종류 Nat의 n이 정확하게 하나의 (잘 정의 된) 값이 들어 (이것은 singletons 라이브러리가 당신을 위해. 생성 다소간 코드입니다) Natty n을 입력하십시오. Natty의 패턴 일치는 n에 대해 알려줍니다. forall n. Natty n -> 한정 기호는 런타임에 n이 사용됨을 알려줍니다. 따라서 우리의 vreplicate 함수는 Natty n -> a -> Vec n a 유형을 가지며 n의 런타임 대기 시간은 Natty n입니다. (실제로 의존적으로 형식화 된 언어를 사용하면 그러한 후프를 뛰어 넘지 못할 것입니다!)

Natty의 값을 알고 있다면 n을 알 수 있습니다. 우리는 추가 정보는 다음 해키 형 클래스를 사용하여, 값 유형에서, 다른 방법으로 흐를 수 :

class NATTY n where 
    natty :: Natty n 
instance NATTY Z where 
    natty = Zy 
instance NATTY n => NATTY (S n) where 
    natty = Sy natty 

NATTY n 사전 n의 싱글 Natty의 암시 복사본입니다.

확인.Vec에 대한 Applicative 인스턴스는 두 벡터를 압축하여 그 내용을 포인트별로 결합합니다.

vzip :: Vec n a -> Vec n b -> Vec n (a, b) 
vzip VNil VNil = VNil 
vzip (x :> xs) (y :> ys) = (x, y) :> vzip xs ys 

vreplicate :: Natty n -> a -> Vec n a 
vreplicate Zy _ = VNil 
vreplicate (Sy n) x = x :> vreplicate n x 

instance NATTY n => Applicative (Vec n) where 
    pure = vreplicate natty 
    fs <*> xs = fmap (uncurry ($)) (vzip fs xs) 

그래서 우리는 a의 벡터에 대한 Monoid로 Monoida에 대한의를 올릴 수있다. Applicative을 Monoid으로 바꾸는 표준 트릭입니다.

instance Monoid a => Monoid (Vec n a) where 
    mempty = pure mempty 
    mappend = liftA2 mappend 

보수 : mappend 길이가 일치하는 벡터 만 가능합니다. 이것을 zip 목록과 비교해보십시오.이 목록은 압축 된 두 목록 중 긴 것을 자릅니다.

ghci> v1 `mappend` v2 
"foobaz" :> ("barquux" :> VNil) 

-- ┌  ┐  ┌  ┐  ┌   ┐ 
-- | "foo" | + | "baz" | = | "foobar" | 
-- | "bar" |  | "quux" |  | "bazquux" | 
-- └  ┘  └  ┘  └   ┘ 

ghci> v1 `mappend` v3 
<interactive>:35:14: error: 
    • Couldn't match type ‘'Z’ with ‘'S 'Z’ 
     Expected type: Vec Two String 
     Actual type: Vec One String 
    • In the second argument of ‘mappend’, namely ‘v3’ 
     In the expression: v1 `mappend` v3 
     In an equation for ‘it’: it = v1 `mappend` v3 

-- ┌  ┐  ┌   ┐ 
-- | "foo" | + | "nabble" | = ? 
-- | "bar" |  └   ┘ 
-- └  ┘ 

---

이제 2D 매트릭스와 함께 작동 할 수 있습니다. 트릭은 재사용이 가능한 작은 비트로 구성하는 것입니다. 행렬은 두 벡터의 유형 수준 구성 인 벡터 벡터입니다. 이다

newtype (f :.: g) a = Compose { getCompose :: f (g a) } deriving Show 

type Mat n m = Vec n :.: Vec m 

, Mat n m a는 Vec n (Vec m a) 동형이다.

Functoriality 및 applicativity는 구성을 통해 보존,

instance (Functor f, Functor g) => Functor (f :.: g) where 
    fmap f = Compose . fmap (fmap f) . getCompose 
instance (Applicative f, Applicative g) => Applicative (f :.: g) where 
    pure = Compose . pure . pure 
    Compose fgf <*> Compose fgx = Compose (liftA2 (<*>) fgf fgx) 

우리는 한 번 더 구성 Applicative의의 Applicative에 Monoid를 들어 올릴 수있는 표준 트릭을 사용 할 수 있습니다.

instance (Monoid a, Applicative f, Applicative g) => Monoid ((f :.: g) a) where 
    mempty = pure mempty 
    mappend = liftA2 mappend 

이제 우리는 무료로 매트릭스 추가를 얻습니다!

m1 :: Mat Two Two String 
m1 = Compose (v1 :> v2 :> VNil) 
m2 :: Mat Two Two String 
m2 = Compose (v2 :> v1 :> VNil) 

ghci> m1 `mappend` m2 
Compose {getCompose = ("foobaz" :> ("barquux" :> VNil)) :> (("bazfoo" :> ("quuxbar" :> VNil)) :> VNil)} 

-- ┌    ┐  ┌    ┐  ┌     ┐ 
-- | "foo" "bar" | + | "baz" "quux" | = | "foobaz" "barquux" | 
-- | "baz" "quux" |  | "foo" "bar" |  | "bazfoo" "quuxbar" | 
-- └    ┘  └    ┘  └     ┘ 

mempty 같은 행렬과 행렬 승산을 수행한다 (사각형 행렬 들면 newtype Square n = Square (Mat n n)) 다른 유효한 매트릭스 Monoid있다. 나는 그것을 여기에 보여주지 않을 것이다. 너 스스로 알아낼 수있어.

---

마지막의이 N 차원 행렬이다 텐서의 추가를 할 수 있습니다. 텐서는 차원 목록에 의해 인덱싱 된 유형의 패밀리입니다. 즉, Tensor은 함수이고 차원 목록에서 형식 생성자 * -> *입니다. 목록에 새 치수를 추가하면 Vec의 레이어가 추가됩니다.

type family Tensor (dims :: [Nat]) :: * -> * where 
    Tensor '[d] = Vec d 
    Tensor (d ': ds) = Vec d :.: Tensor ds 

그래서, Tensor '[One, Two, Three] a, 하나의 별이 별 세 텐서는 Vec One (Vec Two (Vec Three a))에 -isomorphic newtype입니다.

Vec 및 :.:으로 다시 정의하면 Tensor은 무료로 필요한 인스턴스를 얻게됩니다.

t1 :: Tensor '[Two, Two, Two] String 
t1 = Compose (m1 :> m2 :> VNil) 
t2 :: Tensor '[Two, Two, Two] String 
t2 = Compose (m2 :> m1 :> VNil) 

ghci> t1 `mappend` t2 
Compose {getCompose = Compose {getCompose = ("foobaz" :> ("barquux" :> VNil)) :> (("bazfoo" :> ("quuxbar" :> VNil)) :> VNil)} :> (Compose {getCompose = ("bazfoo" :> ("quuxbar" :> VNil)) :> (("foobaz" :> ("barquux" :> VNil)) :> VNil)} :> VNil)} 

-- i'm not going to try drawing that