По умолчанию переменные промежуточного типа - PullRequest
Новая
       73

По умолчанию переменные промежуточного типа

2 голосов
/ 08 июля 2019

Я бы хотел представить список из (before, during, after) пар, такой что all (\(_, _, after), (before, _, _) -> after == before) $ zip xs (tail xs);другими словами, так, что соседние пары совпадают на своих концах.Конечная цель состоит в том, чтобы извлечь свернутый список (before, [(during, after)].

. Мы можем легко реализовать это, используя Star -подобную структуру для обеспечения соответствия концов: 

{-# LANGUAGE GADTs, PolyKinds, DataKinds, KindSignatures, TypeApplications, ScopedTypeVariables #-}

import Data.Singletons

data Step a (before :: ending) (after :: ending) where
    Step :: (SingI before, SingI after) => a -> Step a before after

infixr 5 :>
data Steps a (first :: ending) where
    Nil :: Steps a first
    (:>) :: Step a before after -> Steps a after -> Steps a before

before :: forall ending a (before :: ending) (after :: ending). (SingKind ending) => Step a before after -> Demote ending
before Step{} = FromSing (sing @before)

after :: forall ending a (before :: ending) (after :: ending). (SingKind ending) => Step a before after -> Demote ending
after Step{} = FromSing (sing @after)

collapse :: forall ending a (first :: ending). (SingKind ending) => Steps a first -> (Maybe (Demote ending), [(a, Demote ending)])
collapse Nil = (Nothing, [])
collapse xs@(x :> _) = (Just $ before x, go xs)
  where
    go :: Steps a whatever -> [(a, Demote ending)]
    go Nil = []
    go (s@(Step x) :> xs) = (x, after s) : go xs

Пример использования: 

{-# LANGUAGE TemplateHaskell, PatternSynonyms, TypeFamilies, StandaloneDeriving #-}
import Data.Singletons.TH

$(singletons [d|
  data Ending = A | B | C
  |])
deriving instance Show Ending

foo :: Steps Int A
foo =
    Step @A @B 1 :>
    Step @B @C 2 :>
    Nil

> collapse foo
(Just A,[(1,B),(2,C)])

Пока все хорошо.

Но теперь, скажем, некоторые из этих Step s дондействительно не заботятся об их окончаниях.Хотя мы можем позволить выводу типа заполнить их там, где они недвусмысленны, например, 

example1 :: Steps Int A
example1 =
    Step 1 :>
    Step @B @C 2 :>
    Nil

Но это ломается, если не хватает ограничений для устранения неоднозначности, например, это не удается: 

example2 :: Steps Int A
example2 =
    Step 1 :>
    Step 2 :>
    Step @B @C 3 :>
    Nil

Неопределенная переменная типа after0, возникающая в результате использования Step, препятствует решению ограничения (SingI after0).

Понятно, что это не может быть выполнено;например, не было бы места, из которого мы могли бы извлечь ending, который мы поместили в список collapse d.

Вместо этого мы можем сделать явное выражение "безразличия", используя Maybe endingс обеих сторон: 

data Step a (before :: Maybe ending) (after :: Maybe ending) where
    Step :: (SingI before, SingI after) => a -> Step a before after

data Steps a (first :: Maybe ending) where
    Nil :: Steps a first
    (:>) :: Step a before after -> Steps a after -> Steps a before
infixr 5 :>

before :: forall ending a (before :: Maybe ending) (after :: Maybe ending). (SingKind ending) => Step a before after -> Maybe (Demote ending)
before Step{} = FromSing (sing @before)

after :: forall ending a (before :: Maybe ending) (after :: Maybe ending). (SingKind ending) => Step a before after -> Maybe (Demote ending)
after Step{} = FromSing (sing @after)

collapse :: forall ending a (first :: Maybe ending) . (SingKind ending) => Steps a first -> (Maybe (Demote ending), [(a, Maybe (Demote ending))])
collapse Nil = (Nothing, [])
collapse xs@(x :> _) = (before x, go xs)
  where
    go :: Steps a whatever -> [(a, Maybe (Demote ending))]
    go Nil = []
    go (s@(Step x) :> xs) = (x, after s) : go xs

, а затем явно смоделируйте связь между Nothing и Just ending, ослабляя при необходимости: 

type family Meet (a :: Maybe k) (b :: Maybe k) where
    Meet Nothing  b        = b
    Meet a        Nothing  = a
    Meet (Just a) (Just a) = Just a

infixr 5 >:>
(>:>) :: forall before after after' meet a. (Meet after after' ~ meet, SingI meet) => Step a before after -> Steps a after' -> Steps a before
Step x >:> xs = Step x :> xs'
  where
    xs' :: Steps a meet
    xs' = case xs of
        Nil -> Nil
        Step y :> ys -> Step y :> ys

Это позволяет нам переписать example2, используяNothing s для представления окончаний без ограничений: 

example2 :: Steps Int (Just A)
example2 =
    Step @(Just A) @Nothing 1 >:>
    Step @Nothing  @Nothing 2 >:>
    Step @(Just B) @(Just C) 3 >:>
    nil

> collapse example2
(Just A,[(1,Nothing),(2,Just B),(3,Just C)])

Итак, теперь мой вопрос

Возможно лиубрать необходимость в явных приложениях типа @Nothing?То есть есть какая-то инфраструктура, которую я мог бы добавить, которая бы означала следующее значение, аналогичное example2 выше: 

example2' :: Steps Int (Just A)
example2' =
    Step @(Just A) 1 >:>
    Step 2 >:>
    Step @(Just B) @(Just C) 3 >:>
    nil

?

...