библиотека экзистенциальных обертках типа

Question

Допустим, у меня есть следующие:

data T a 

f :: a -> (exists t. T t) 
g :: T b -> c 

h :: a -> c 
h = g . f 

Как я знаю, тип подписи для f не является действительным Haskell. Вместо этого я могу сделать это:

{-# LANGUAGE GADTs #-} 

data T a 

data ExistsTA where 
    ExistsTA :: T a -> ExistsTA 

f :: a -> ExistsTA 
g :: T b -> c 

h :: a -> c 
h x = case (f x) of ExistsTA x' -> g x' 

Который компилирует в порядке. Мне было интересно, есть ли библиотека, которая обобщает создание типа данных ExistsTA (возможно, в качестве параметра принимает значение T), или мне нужно каждый раз откатывать свой собственный каждый раз, когда я хочу это сделать (что не очень важно, просто дон Не хочу, чтобы изобретать колесо, если мне тоже не нужно).

В частности, для моего приложения, я также хотел бы упаковщик в таком виде:

data C where 
    C1 :: C 
    ... 

data D (a :: C) where 
    D1 a :: D 
    ... 

data T (d :: D) a 

f :: T (D1 C1) a -> exists c. T (D1 c) a 

Answer 1

Я не знаю, является ли это в библиотеке в любом месте, но я хотел бы использовать следующее общее назначение экзистенциальным:

data Ex f = forall a. Ex (f a) 

с PolyKindsEx может экзистенциально завернуть параметр любого типа f :: k -> *. Как это общего? Мы можем манипулировать f до тех пор, пока это не будет правильной формой, и мы сможем создать любую дополнительную информацию, которая нам нужна, с небольшой библиотекой комбинаторов типов. Работа с такими типами общего назначения, как это, является мощным способом программирования, но часто проще просто сворачивать свои собственные.

---

Предположим, что мы хотим, чтобы экзистенциально количественно обе половинки типа два параметра p. Можно использовать следующий GADT до uncurryp, превратив его из двухпараметрического типа k1 -> k2 -> * в однопараметрический тип (k1, k2) -> *.

data Uncurry p ij where 
    Uncurry :: { getUncurry :: p i j } -> Uncurry p '(i, j) 

Теперь Uncurry p может быть экзистенциально завернуты.

type ExP p = Ex (Uncurry p) 

---

Предположим, я хочу, чтобы установить соединение между экзистенциально-обернутый типа с некоторыми доказательствами, такие как синглтон, так что можно восстановить экзистенциально количественных индексов. Я буду использовать индекс уважающей продукта на пары два функтора f и g:

newtype (f :*: g) i = f i :*: g i 

Если, скажем, f является GADT, шаблон сопоставление на f суммы половины пары расскажет вам о g индекс. Теперь f :*: g имеет правильный вид, который может быть экзистенциально завернут.

type ExPair f g = Ex (f :*: g) 

На практике вы можете написать ExPair Sing f в паре f с одноплодной.

---

Предположим, мне нужны вышеупомянутые доказательства в форме ограничения.Я могу заменить Sing сверху следующего типа, который материализует словарь экземпляра для c a как (видимые) значения времени выполнения:

data Dict1 c a where 
    Dict1 :: c a => Dict1 c a 

(или вы можете использовать the constraints package:. newtype Dict1 c a = Dict1 { getDict1 :: Dict (c a) }) Теперь мне просто нужно, чтобы установить левые -hand часть моей пары быть Dict1 c:

type ExDictPair c f = ExPair (Dict1 c) f 

Таким образом, вы могли бы написать ExDictPair SingI f упаковать неявный синглтон.

---

Предположим, что мне нужно экзистенциально количественно на более высоком виде, например * -> *. (Возможно, я хочу поговорить о «некотором экземпляре Monad, содержащем Int».) Ex является многоподобным, но он только экзистенциально количественно определяет самый правый параметр его аргумента. Поэтому нам нужна часть типа * -> *, которая будет последним аргументом нашего типа данных. Я также могу написать комбинатор типов:

newtype RApp a f = RApp { getRApp :: f a } 

type SomeMonadAppliedToInt = ExDictPair Monad (RApp Int)