Как использовать библиотеку toSing from singletons? - PullRequest
Новая
       41

Как использовать библиотеку toSing from singletons?

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

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

Мне удалось использовать fromSing успешно преобразовать «тип синглтона» в «термин уровня значения» (правильна ли моя терминология?) Однако я не могу понять, как использовать toSing и концептуально , как это будет конвертироватьзначение во время выполнения для типа?

Вот что говорят документы для toSing, чего я не очень понимаю ... 

-- Convert an unrefined type to an existentially-quantified singleton type.
toSing :: Demote k -> SomeSing k

Вот что SomeSing говорит: 

-- An existentially-quantified singleton. This type is useful 
-- when you want a singleton type, but there is no way of knowing, 
-- at compile-time, what the type index will be. To make use of this 
-- type, you will generally have to use a pattern-match:

foo :: Bool -> ...
foo b = case toSing b of
          SomeSing sb -> {- fancy dependently-typed code with sb -}

Означает ли это, что концептуально , fromSing в основном делает следующее: 

data RuntimeValue = Value1 | Value2

someFunction :: RuntimeValue -> UnifiedType a
case runtimeValue of
  Value1 -> someAction (Proxy :: Proxy 'Value1)
  Value2 -> someAction (Proxy :: Proxy 'Value2)

И это лучшее, что можно ожидать от Haskell, на сегодняшний день?то есть нам нужно сопоставить с образцом значение времени выполнения, запустить функции, которые могут быть разных типов, но в конечном итоге они должны объединиться в один тип?

1 Ответ

3 голосов
/ 09 июля 2019

Если вы скомпилируете код: 

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module SingletonExample where
import Data.Singletons.TH
singletons [d| data Value = Value1 | Value2 |]

с флагами -ddump-splices -dsuppress-uniques, вы увидите фактический код, который библиотека singletons генерирует через Template Haskell.В частности, сгенерированный экземпляр SingKind имеет вид: 

instance SingKind Value where
  type Demote Value = Value
  fromSing SValue1 = Value1
  fromSing SValue2 = Value2
  toSing Value1 = SomeSing SValue1
  toSing Value2 = SomeSing SValue2

Таким образом, fromSing и toSing являются просто шаблонными функциями преобразования из (времени выполнения) значений в (время выполнения) синглетонов и обратно.

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

g :: SValue value -> String
g SValue1 = "one"
g SValue2 = "two"

, но все, что у вас есть, - это соответствующее значение.В этом случае вы можете использовать несколько неловкую конструкцию: 

f :: Value -> String
f v = case toSing v of SomeSing sv -> g sv

для вызова g с необходимым синглтоном.

Оказывается, что для обычных случаев использования для синглетоновЕсть только несколько ситуаций, когда это работает и / или полезно.В результате на самом деле довольно редко можно увидеть toSing, используемый в одноэлементном коде.И, в частности, нет необходимости или очень часто особенно полезно использовать toSing при работе с типами, зависящими от времени выполнения.

В конечном счете, если вы хотите изучить / понять библиотеку singletons, выНужно понимать, когда и почему синглеты полезны (и в сложном и тонком смысле, в котором они являются представлениями типов во время выполнения), а не как конвертировать туда и обратно между ними и их связанными значениями.Для этого я предлагаю прочитать статью Hasochism , Программирование с независимой типизацией с помощью синглетонов , выполнить поиск "Программы с зависимой типизацией в haskell" и / или "Haskell Singletons" и прочитать каждое сообщение в блоге, которое выувидеть.У Weirich есть видео на YouTube , которые тоже стоит посмотреть.

...