Тип Juggling с Existentials в Runtime

Question

Я играю с экзистенциальными и GADT в Haskell, и я пытаюсь определить DSL для комбинаторов (например, SKI). Я имею работу GADT, а также функцию восстановления, которая отлично работает (и на самом деле не относятся к вопросу)

{-# LANGUAGE GADTs, ExistentialQuantification #-} 

import Control.Applicative 
import Data.Monoid 
import Control.Monad 

data Comb t where 
    S :: Comb ((a -> b -> c) -> (a -> b) -> a -> c) 
    K :: Comb (a -> b -> a) 
    I :: Comb (a -> a) 
    B :: Comb ((b -> c) -> (a -> b) -> a -> c) 
    C :: Comb ((b -> a -> c) -> a -> b -> c) 
    W :: Comb ((a -> a -> b) -> a -> b) 
    (:$) :: Comb (a -> b) -> Comb a -> Comb b 

То, что я пытаюсь сделать теперь определить способ чтения комбинаторов строк в от пользователя во время выполнения. Очевидно, для этого мне нужен экзистенциальный тип, поскольку информация типа GADT должна быть скрыта.

data CombBox = forall a. CombBox { unCombBox :: Comb a } 

($$) :: CombBox -> CombBox -> Maybe CombBox 
x $$ y = undefined -- ??? 

Я хотел бы функцию ($$) какой-то образом «заглянуть внутрь» в CombBox экзистенциалов во время выполнения, и, если можно объединить два комбинаторов с помощью :$ и получить хорошо напечатанный результат, я хотел бы результат быть этим. В противном случае, я хочу Nothing. Так, например,

CombBox S $$ CombBox K ==> Just (CombBox (S :$ K)) 
CombBox W $$ CombBox I ==> Nothing 

Последние должны не потому, что W ожидает 2-кратную функцию где I принимает один аргумент. Но я бы хотел отменить эту проверку во время выполнения, и я не уверен, что такая возможность возможна в системе типов Haskell (+ GHC extensions).

Answer 1

Приготовьтесь к изучению зависимых пар и singleletons!

---

Я собираюсь переписать систему немного, чтобы упростить ее.

Во-первых, я собираюсь сжать вашу вселенную типов от всех Haskell к гораздо более простой вселенной, состоящей из одного примитивного типа и стрелок.

infixr 0 :-> 
data Type = Unit | Type :-> Type 

Надеюсь, вы должны уметь видеть, как расширить это с помощью более примитивных типов.

Я также удалю большую часть бит из Comb, так как они могут быть выражены в терминах друг друга.

data Comb a where 
    S :: Comb ((a :-> b :-> c) :-> (a :-> b) :-> a :-> c) 
    K :: Comb (a :-> b :-> a) 
    (:$) :: Comb (a :-> b) -> Comb a -> Comb b 

i = S :$ K :$ i 
b = (S :$ (K :$ S)) :$ K 
c = S :$ (S :$ (K :$ (S :$ (K :$ S) :$ K)) :$ S) :$ (K :$ K) 
w = S :$ S :$ (S :$ K) 

---

Теперь к вашему вопросу. Как вы правильно поняли, когда вы читаете пользовательский ввод, вы не можете заранее предсказать, какой тип результирующего термина будет, так что вам нужно его количественно оценить.

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

Проблема заключается в следующем: как вы восстанавливаете информацию о типе, чтобы иметь возможность манипулировать условиями? Мы можем связать Comb с другим значением, которое вы можете сопоставлять шаблону во время выполнения до . Изучите тип Comb. Вот комбинатор для спаривания вещей.

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

(я поднял оба этих типов из the Hasochism paper.) :*: пара до двух типов, обеспечивающих, что их индексы равны.Мы будем использовать его вместе с Ex для имитации зависимой пары или sigma Тип: пара значений, для которых тип второго компонента зависит от значения первого. Идея состоит в том, что f будет GADT, который сообщает вам что-то о своем индексе, поэтому сопоставление шаблонов на f дает вам информацию о типе g.

type Sg f g = Ex (f :*: g) 
pattern Sg x y = Ex (x :*: y) 

Теперь умная часть: придумал GADT, в котором рассказывается о типе комбинаторного термина.

data Typey t where 
    Unity :: Typey Unit 
    Arry :: Typey a -> Typey b -> Typey (a :-> b) 

Typey называется одноточечно. Для данного t существует ровно одно значение типа Typey t. Поэтому, если у вас есть значение Typey t, вы знаете все, что нужно знать о t.

Синглтонские значения в конечном счете являются взломом. Typey не Type; это резервная копия уровня данных для дублированной копии типа Type. В реальной системе с типичным типом вам не нужен одноэлементный клей для прикрепления материала уровня ценности к материалам типа, потому что различия там нет.

Наши экзистенциально-количественные комбинаторы теперь выглядят так. AComb упаковывает Comb с представлением времени выполнения. Этот метод позволяет гарантировать, что в коробке Comb хорошо напечатан; мы просто не можем сказать статически, что это за тип.

type AComb = Sg Typey Comb 

---

Как мы пишем ($$), который пытается применить AComb к другому AComb? Нам нужно сопоставить шаблон по связанным с ними Typey с, чтобы узнать, можно ли применять одно к другому. В частности, нам понадобится способ узнать, равны ли два типа.

Приходит Пропозициональное равенство, доказательство GADT, что две вещи уровня уровня равны. Вы можете указать значение Refl, если вы можете объяснить GHC, что a и b на самом деле то же самое. И наоборот, если вы сопоставляете шаблон по Refl, тогда GHC добавит a ~ b в контекст ввода.

data a :~: b where 
    Refl :: a :~: a 
withEq :: a :~: b -> (a ~ b => r) -> r 
withEq Refl x = x 

Вот функция помощника, чтобы поднять пару равенств через :-> конструктора.

arrEq :: (a :~: c) -> (b :~: d) -> (a :-> b) :~: (c :-> d) 
arrEq Refl Refl = Refl 

Как и было обещано, мы можем записать функцию, чтобы проверить, являются ли два Type s равны. Мы продолжаем с помощью сопоставления шаблонов на их ассоциированном одноэлементном Typey с, если не найти типы, которые несовместимы. Если тест равенства преуспевает, трофеи являются доказательством того, что типы равны.

tyEq :: Typey t -> Typey u -> Maybe (t :~: u) 
tyEq Unity Unity = Just Refl 
tyEq (Arry a b) (Arry c d) = liftA2 arrEq (tyEq a c) (tyEq b d) 
tyEq _ _ = Nothing 

withTyEq :: Typey t -> Typey u -> (t ~ u => a) -> Maybe a 
withTyEq t u x = fmap (\p -> withEq p x) (tyEq t u) 

И наконец, мы можем написать $$.Правило типизации выглядит следующим образом:

f : a -> b y : a 
------------------- App 
     f y : b 

То есть, если левая часть из $$ является типом функции и типа термина правого соответствует домену функции, мы можем ввести приложение. Поэтому для реализации этого правила необходимо проверить (используя withTyEq) соответствие соответствующих типов, чтобы вернуть итоговый термин.

($$) :: AComb -> AComb -> Maybe AComb 
Sg (Arry a b) x $$ Sg t y = withTyEq a t $ Sg b (x :$ y) 
_ $$ _ = Nothing 

---

Генерация Typey терминов соответствует акту проверки типа. Другими словами, функция parse :: String -> AComb должна выполнять как синтаксический анализ , так и. В реальных компиляторах эти две фазы разделены.

Таким образом, я бы посоветовал разобрать вход пользователя в текстовое дерево , которое допускает неработающие термины, а затем генерирует информацию для ввода отдельно.

data Expr = S | K | Expr :$ Expr 
parse :: String -> Parser Expr 
typeCheck :: Expr -> Maybe AComb 

Весело упражнения (в более зависимым от типизированных языков) является изменение typeCheck возвращать более подробное объяснение того, почему тип проверки не удалось, как этот бит псевдо-Agda:

data Void : Set where 
Not : Set -> Set 
Not a = a -> Void 

data TypeError : Expr -> Set where 
    notArr : Not (IsFunction f) -> TypeError (f :$ x) 
    mismatch : Not (domain f :~: type x) -> TypeError (f :$ x) 
    inFunc : TypeError f -> TypeError (f :$ x) 
    inArg : TypeError x -> TypeError (f :$ x) 

typeCheck : (e : Expr) -> Either (TypeError e) AComb 

Вы также можете сделать typeCheck более точным, убедившись, что он не изменит срок, который вы ему даете (другое упражнение).

Для дальнейшего ознакомления см. The View from the Left, в котором имеется проверенная проверка типа для лямбда-исчисления.

Answer 2

Не правильный ответ, но может быть полезным.

Параметричность не позволяет потоку управления зависать от типов, поэтому вам нужно некоторое представление типов первого порядка. Haskell имеет Typeable:

deriving instance Typeable Comb 

data CombBox = forall a. Typeable a => CombBox { unCombBox :: Comb a } 

С его помощью можно определить

castApply1 :: (Typeable a, Typeable b, Typeable ab) => Comb ab -> Comb a -> Maybe (Comb b) 
castApply1 f x = (:$ x) <$> cast f 

Однако

($$) :: CombBox -> CombBox -> Maybe CombBox 
CombBox f $$ CombBox x = CombBox <$> castApply f x 

бросает

Could not deduce (Typeable a0) arising from a use of `CombBox' … 
    from the context (Typeable a) 
    or from (Typeable a1) 
    The type variable `a0' is ambiguous 

Проблема заключается в том, что b указан в е e возвращаемый тип castApply1, но если мы немедленно применим CombBox к castApply f x, то b не указывается и, следовательно, остается неоднозначным.

Мы можем указать b путем предоставления Proxy b в качестве аргумента:

castApply2 :: (Typeable a, Typeable b, Typeable ab) => Proxy b -> Comb ab -> Comb a -> Maybe (Comb b) 
castApply2 p = castApply1 

Что позволяет обернуть результат в CombBox:

castApply3 :: (Typeable a, Typeable b, Typeable ab) => Proxy b -> Comb ab -> Comb a -> Maybe CombBox 
castApply3 p f x = CombBox <$> castApply2 p f x 

Мы можем, наконец, определить то, что не говоря уже о том, что раздражает b:

data SomeTypeable = forall a. Typeable a => SomeTypeable (Proxy a) 

castApply4 :: (Typeable a, Typeable ab) => SomeTypeable -> Comb ab -> Comb a -> Maybe CombBox 
castApply4 (SomeTypeable p) = castApply3 p 

Теперь имея

typeRepToSomeTypeable :: TypeRep -> SomeTypeable 

Мы можем определить

castApply :: (Typeable a, Typeable ab) => TypeRep -> Comb ab -> Comb a -> Maybe CombBox 
castApply t = castApply4 (typeRepToSomeTypeable t) 

($$) :: CombBox -> CombBox -> Maybe CombBox 
CombBox f $$ CombBox x = funResultTy (typeRep f) (typeRep x) >>= \t -> castApply t f x 

funResultTy является функцией в Data.Typeable, которая возвращает кообласть первого аргумента, если его домен совпадает со вторым аргументом.

Но как определить typeRepToSomeTypeable? Кажется, что это не было реализовано. По крайней мере, я не нашел его ни в Data.Typeable, ни в Singletons.