Неправильный вид в `symbolVal` для получения строки уровня типа во время выполнения - PullRequest
0 голосов
/ 16 декабря 2018

Я пытаюсь понять, как работать со строками уровня типа в Haskell.У меня есть тип данных, объявленный следующим образом:

data MyType (s :: Symbol) t = MyType t

Думайте о нем как о значении типа t, помеченном каким-либо образом.

Теперь, когда вы пытаетесь использовать symbolVal,Я получаю ошибку, которую не понимаю.Рассмотрим этот код:

func :: KnownSymbol s => MyType s t -> String
func _ = symbolVal (Proxy :: Proxy s)

Код вызывает следующую ошибку компиляции:

file.hs:63:21: error:
    • Couldn't match kind ‘*’ with ‘Symbol’
      When matching types
        proxy0 :: Symbol -> *
        Proxy :: * -> *
      Expected type: proxy0 n0
        Actual type: Proxy s0
    • In the first argument of ‘symbolVal’, namely ‘(Proxy :: Proxy s)’
      In the expression: symbolVal (Proxy :: Proxy s)
      In an equation for ‘func’: func _ = symbolVal (Proxy :: Proxy s)
   |
63 | func _ = symbolVal (Proxy :: Proxy s)
   |

Я понятия не имею, что я делаю здесь неправильно.Если я пишу Proxy "hello" вместо Proxy s, код компилируется, и функция фактически возвращает «привет», поэтому, по крайней мере, кажется, что я получаю что-то правильно.

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

Ответы [ 2 ]

0 голосов
/ 16 декабря 2018

Вам нужно включить ScopedTypeVariables и использовать явный forall, иначе вы не ссылаетесь на тот же s:

func :: forall s t . KnownSymbol s => MyType s t -> String
func _ = symbolVal (Proxy :: Proxy s)
0 голосов
/ 16 декабря 2018

Решение Чи выше - правильный способ сделать это.В любом случае, эта, возможно, менее изящная альтернатива без forall также должна работать.

func :: KnownSymbol s => MyType s t -> String
func (_ :: MyType s t)  = symbolVal (Proxy :: Proxy s)

Я забыл об этом и так обошел.Я думаю, что это эквивалентно.

не берите в голову ответ ниже, это далеко ...


{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE EmptyDataDecls #-}

import Data.Proxy
data Symbol 
data MyType (s :: Symbol) t = MyType t

class KnownSymbol (s :: Symbol) where

symbolVal :: Proxy s -> String
symbolVal = undefined

func :: KnownSymbol s => MyType s t -> String
func _ = symbolVal (Proxy :: Proxy s)

Этот тип проверяет здесь.Возможно, это ваше class определение, не указывающее вид?

...