Типы привязки в подписи - PullRequest
Новая
       13

Типы привязки в подписи

0 голосов
/ 10 января 2019

Какой самый прямой способ связать переменную типа при сопоставлении с образцом в Gadt? 

#!/usr/bin/env stack
-- stack script --resolver lts-13.1
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs, ScopedTypeVariables             #-}
{-# LANGUAGE DataKinds   #-}
module Main where
import Data.Proxy
import GHC.TypeLits    
main :: IO ()
main = undefined

data Kind where
  Index :: Symbol -> Kind

data Gadt (f::Kind) where
  Lit :: KnownSymbol s => Gadt ('Index s)

Binding s напрямую потерпит неудачу 

format :: Gadt f -> String
format (Lit :: Gadt ('Index s)) = undefined   -- KO

с ошибкой 

• Couldn't match type ‘f’ with ‘'Index s’
  ‘f’ is a rigid type variable bound by
    the type signature for:
      format :: forall (f :: Kind). Gadt f -> String
  Expected type: Gadt f
  Actual type: Gadt ('Index s)

Функция типа может извлечь тип, но нет ли более прямого способа сделать это? 

format (Lit :: Gadt i)  =  symbolVal (Proxy :: TLabel i)

type family TLabel (a::Kind)
type instance TLabel ('Index s  ) = Proxy s

1 Ответ

0 голосов
/ 10 января 2019

Единственный способ, которым я вижу, это добавить Proxy, чтобы связать переменную типа с ScopedTypeVariables. 

data Gadt a where
  Lit :: KnownNat s => Proxy s -> Gadt ('Index s)

format :: Gadt a -> String
format (Lit (Proxy :: Proxy s)) = undefined

Если вас беспокоит дополнительное выделение, поле можно распаковать. (ПРАВКА: удалено предыдущее упоминание Proxy#, потому что это не кажется необходимым). 

import Data.Proxy

-- This should be as efficient as the original Gadt with a nullary Lit
data Gadt a where
  Lit :: {-# UNPACK #-} !(Proxy r) -> Gadt ('Index r)

format :: Gadt a -> String
format (Lit (_ :: Proxy r)) = undefined

В долгосрочной перспективе следующее предложение GHC решит эту проблему: Тип приложений в шаблонах . 

-- The original type
data Gadt a where
  Lit :: forall s. Gadt ('Index s)

format :: Gadt a -> String
format (Lit @s) = ...
...