Tôi đã thử nghiệm với các chương trình được nhập bằng cách sử dụng thư viện Data.Singletons, theo sau việc phát triển các vectơ được chú thích theo chiều dài trong bài báo, "Lập trình được đánh máy phụ thuộc với Singletons" và tôi đã chạy vào vấn đề sau.Các đối số và loại trừ không hợp lệ
Mã này, không bao gồm định nghĩa của hàm indexI, typechecks trong GHC 7.6.3 và các công trình như mong đợi trong sự vắng mặt của nó:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Singletons
import Data.Singletons.TH
data Nat where
Z :: Nat
S :: Nat -> Nat
deriving Eq
$(genSingletons [''Nat])
data FlipList :: * -> * -> Nat -> * where
Cons :: ((a -> b) -> a -> b) -> FlipList a (a -> b) n -> FlipList a b (S n)
Nil :: FlipList a b Z
type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Z = 'False
type instance Z :< (S n) = 'True
type instance (S m) :< (S n) = m :< n
type family PreMap a b (m :: Nat) :: *
type instance PreMap a b Z = a -> b
type instance PreMap a b (S n) = PreMap a (a -> b) n
type family BiPreMap a b (m :: Nat) :: *
type instance BiPreMap a b m = PreMap a b m -> PreMap a b m
index :: ((m :< n) ~ 'True) => SNat m -> FlipList a b n -> BiPreMap a b m
index SZ (Cons f _) = f
index (SS sm) (Cons _ fl) = index sm fl
indexI :: ((m :< n) ~ 'True, SingI m) => FlipList a b n -> BiPreMap a b m
indexI = withSing index
Sau bao gồm indexI, GHC sản xuất hai lỗi,
Could not deduce (PreMap a b m ~ PreMap a b a0)
from the context ((m :< n) ~ 'True, SingI Nat m)
bound by the type signature for
indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
FlipList a b n -> BiPreMap a b m
và,
Could not deduce (PreMap a b m ~ PreMap a b a0)
from the context ((m :< n) ~ 'True, SingI Nat m)
bound by the type signature for
indexI :: ((m :< n) ~ 'True, SingI Nat m) =>
FlipList a b n -> BiPreMap a b m
Gốc của một trong hai lỗi có vẻ là cụm từ withSing index có loại FlipList a b n -> BiPreMap a b a0 và, mà không thể suy ra a0 ~ m, GHC không thể chứng minh được BiPreMap a b m ~ BiPreMap a b a0. Tôi biết rằng kiểu suy luận về loại gia đình thiếu phần lớn các tiện ích mà chúng ta có được khi làm việc với ADTS (tiêm, phát sinh, vv), nhưng sự hiểu biết của tôi về vấn đề chính xác là gì trong trường hợp này và cách phá vỡ nó. . Có một số hạn chế tôi có thể chỉ định có thể xóa nó?
Tác phẩm sau đây dành cho tôi: 'indexI :: forall m n a b. ((m: FlipList a b n -> BiPreMap a b m; indexI = withSing (chỉ mục :: SNat m -> FlipList a b n -> BiPreMap a b m) ' –
user2407038