Как использовать зависимый парный тип Sigma из библиотеки singletons?

Как зависимая пара может ввести Sigma из синглетонов использовать библиотеку?

Предположим, что существует следующий индексированный список типов и функция репликации:

data Vect :: Nat -> Type -> Type where
  VNil :: Vect 0 a
  VCons :: a -> Vect n a -> Vect (n + 1) a

replicateVec :: forall n a. Sing n -> a -> Vect n a

(Вы можете найти пару различных реализаций replicateVec в этот вопрос).

Я хотел бы создать функцию replicateVecSigma, которая возвращает Vect в зависимой паре. В идеале было бы примерно следующее:

replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)

Как можно использовать Sigma для написания этой функции? А как можно записать тип функции?

На самом деле я могу реализовать replicateVecSigma следующим образом, но это не кажется очень чистым:

data Foo a b (m :: TyFun Nat Type)

type instance Apply (Foo a b) (n :: Nat) = a n b

replicateVecSigma :: Natural -> Sigma Nat (Foo Vect String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

К сожалению, мне приходится объявлять этот тип Foo и экземпляр Apply только для того, чтобы использовать Sigma. Предоставляет ли библиотека singletons способ упростить работу с Sigma?

Вы можете найти мой полный код здесь.

Для полноты вот определение Sigma:

data Sigma (s :: Type) :: (s ~> Type) -> Type where
  (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t

Вот ~>:

type a ~> b = TyFun a b -> *

data TyFun :: * -> * -> *

instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2)

type instance Demote (k1 ~> k2) = Demote k1 -> Demote k2

class SingKind k where
  type family Demote k :: * = r | r -> k
  fromSing :: forall (a :: k). Sing a -> Demote k
  toSing :: Demote k -> SomeSing k

Вот @@:

type a @@ b = Apply a b

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

singletons определяет группу экземпляров для Apply.

Как сделать TyFun и Apply работает?

Вот три вопроса сверху:

  1. Как я могу использовать Sigma для написания такой функции, как replicateVecSigma :: Natural -> Sigma Nat (\n -> Vect n String)?
  2. Я могу написать replicateVecSigma, используя приведенный выше тип Foo, но это слишком много дополнительной работы. Есть ли более простой способ?
  3. Как работают TyFun и Apply?

types singleton-type haskell dependent-type
person illabout    schedule 14.04.2018    source источник
comment
Все эти сложные вещи являются результатом основанного на singletons дефункционализации кодирования функций типов. Автор singletons написал об этом в своем блоге   -  person Benjamin Hodgson♦    schedule 14.04.2018

Ответы (2)


arrow_upward
3
arrow_downward

В этом конкретном случае мы хотим вычислить лямбду на уровне типа

\n -> Vect n String

К сожалению, у нас нет лямбд на уровне типов. В лучшем случае мы можем определить семейства типов, как это сделал ОП. Однако мы можем переписать лямбду в бесточечном стиле:

\n -> flip Vect String n    -- pseudocode
flip Vect String

и мы можем превратить эту идею в фактический тип, используя функцию типа singletons уровня Flip типа. Здесь мы хотим частично применить Flip с двумя аргументами (при насыщенном вызове требуется три), поэтому вместо этого мы используем «дефункционализированный» вариант FlipSym2.

Это компилирует:

replicateVecSigma :: Natural -> Sigma Nat (FlipSym2 (TyCon Vect) String)
replicateVecSigma i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec snat "hello"

Если бы у нас был аргумент n в последней позиции с самого начала, мы могли бы избежать Flip.

data Vect2 :: Type -> Nat -> Type where
  VNil2 :: Vect2 a 0
  VCons2 :: a -> Vect2 a n -> Vect2 a (n + 1)

replicateVec2 :: forall n a. Sing n -> a -> Vect2 a n
replicateVec2 = undefined

replicateVecSigma2 :: Natural -> Sigma Nat (TyCon (Vect2 String))
replicateVecSigma2 i =
  case toSing i of
    SomeSing snat -> snat :&: replicateVec2 snat "hello"

( TyCon Vect2 @@ String также работает здесь, используя явное приложение @@ на дефункционализированном уровне вместо приложения фактического типа.)

Грубо говоря, вы можете думать о дефункционализированных вариантах, таких как FlipSym0, FlipSym1, FlipSym2, как о базовых тегах (не функциях!), без внутреннего смысла, за исключением того факта, что Apply позволяет вам работать с ними, притворяясь, что они функции. Таким образом, мы можем работать с нефункциями («тегами»), как если бы они были функциями. Это необходимо, так как в Haskell у нас нет функций на уровне типов, поэтому нам приходится работать с этими «притворными» версиями.

Подход общий, но требует от программиста больше работы, чем хотелось бы.

Я не знаю ни одной утилиты Template Haskell, которая может автоматически преобразовывать лямбда-выражения на уровне типов в бесточечную форму, а затем дефункционализировать их. Это было бы весьма полезно.

person chi    schedule 14.04.2018
comment
Я думаю, вы использовали TyCon, когда вам нужно было использовать TyCon2 несколько раз? - person HTNW; 14.04.2018
comment
@HTNW Я тоже так думал, но мой код все равно скомпилировался. Теперь я вижу, что TyCon — это data family, который автоматически обрабатывает арность. В его документе на github указана рабочая лошадка для типов «TyCon1» и т. Д. Его можно использовать непосредственно вместо любого из типов @TyConN@, но он будет работать только с типами /monomorphic/. Когда GHC#14645 будет исправлен, это должно полностью заменить типы @TyConN@. - person chi; 14.04.2018

arrow_upward
3
arrow_downward

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

Например, ваш Foo a b — это символ, кодирующий функцию \n -> a n b.

Другой способ получить эквивалентный символ — следовать интуиции, что (\n -> a n b) = flip a b.

Обратите внимание, что конструкторы типов, такие как Vec, сами по себе не являются символами, которые могут быть переданы в Apply, но должны быть заключены в «конструкторы символов»: TyCon2 Vec — это символ для \n -> \b -> Vec n b.

singletons имеет символ для flip, FlipSym0 (символы могут обозначать функции более высокого порядка, принимая другие символы в качестве аргументов).

Foo a b = Apply (Apply FlipSym0 (TyCon2 a)) b

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

        = Apply (FlipSym1 (TyCon2 a)) b
        = FlipSym2 (TyCon2 a) b

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

См. также этот пост в блоге Ричарда Айзенберга о дефункционализации типов Haskell: https://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-win/

person Li-yao Xia    schedule 14.04.2018