Распакуйте Existentials в Existential Type - PullRequest
Новая
       39

Распакуйте Existentials в Existential Type

0 голосов
/ 29 октября 2018

Я пытался написать следующий код: 

{-# LANGUAGE GADTs #-}

module V where

data V a where
  V :: (c -> a) -> V a

down :: V (V a) -> V a
down (V f) = V $ \(c,d) -> case f c of
  V f' -> f' d

Тогда GHC ответил type variable `c' would escape its scope.

Я понимаю, почему он не компилируется: он использует скрытый тип экзистенции из case.

Но на самом деле тип все еще скрыт от V. так что, по сути, у функции down нет проблем, я думаю.

Есть ли способ написать скомпилируемую down функцию?

Ответы [ 3 ]

0 голосов
/ 30 октября 2018

В Хаскеле я не могу найти простой способ заставить ваш код работать.

Мне кажется интересным, что ваша идея работает на языке с полностью зависимыми типами, такими как Coq (и, вероятно, Agda, Idris и т. Д.).

Основной смысл, как указывает Даниэль Вагнер, состоит в том, что тип, полученный из f, может зависеть от значения c, поэтому пара (c,d) в исходном коде должна быть зависимой парой .

Для чего это стоит, вот как мы можем сделать это в Coq.

Обратите внимание, что это не относится к необитаемому типу, например forall a. a. 

(* An existential type, under an impredicative encoding *)
Inductive V (A: Type): Type :=
  Vk : forall (B: Type), (B -> A) -> V A
.

(* The usual "identity to equivalence" *)
Definition subst {A B: Type} (p: A = B) (x: A): B :=
   match p with
   | eq_refl => x
   end .

(* The main function.

   Essentially, we want to turn
     Vk B (fun b => Vk C g)
   into
     Vk (B*C) (fun (b,c) => g c)
   but both C and g can depend on (b:B), so (B*C)
   should be a Sigma type {b:B & ty b}.

*)
Definition down (A: Type) (x: V (V A)): V A :=
   match x with
   | Vk B f => let
      ty (z: V A): Type := match z with | Vk C g => C end
      in Vk A {b:B & ty (f b)} (fun w =>
         match w with
         | existT b y =>
            match f b as o return ty (f b) = ty o-> A with
            | Vk C g => fun (h: ty (f b) = C) =>
               g (subst h y)
            end eq_refl
         end )
   end .
0 голосов
/ 04 ноября 2018

Спасибо за еще один отличный ответ, Чи!

Я переписал код для Agda, и на самом деле он компилируется. В качестве дополнительного примечания к приведенному выше ответу я размещаю свой код здесь. 

module down where

open import Level
open import Data.Product

data V {ℓ} (A : Set ℓ) : Set (suc ℓ) where
  Vk : {B : Set} → (B → A) → V A

down : ∀ {ℓ} {A : Set ℓ} → V (V A) → V A
down {ℓ} {A} (Vk {B} f) = Vk go where
  ty : V A → Set
  ty (Vk {C} _) = C
  go : Σ B (λ b → ty (f b)) → A
  go (b , c) with f b
  go (b , c) | Vk {C} g = g c
0 голосов
/ 29 октября 2018

Вот фундаментальная проблема: f может взглянуть на c и использовать значение c, чтобы определить, какой тип скрыть в его экзистенциальности. Например: 

v :: V (V Int)
v = V $ \p -> case p of
     False -> V (id :: Int -> Int)
     True  -> V (fromEnum :: Char -> Int)

Так что d должно быть и действительным Int, и действительным Char, если бы мы позвонили down v! Чтобы иметь возможность подавать экзистенциал, который может быть настолько переменным, вам необходимо убедиться, что его аргумент может принимать все типы, которые он может требовать. 

newtype Forall = Forall (forall a. a)

down :: V (V a) -> V a
down (V f) = V $ \(c, d_) -> case f c of
    V f' -> case d_ of
        Forall d -> f' d
...