Жонглирование вводом с помощью GADT во время выполнения

Я разрабатываю типизированный формальный язык, то есть формальный язык, в котором каждая буква имеет представление определенного типа. Пока что у меня есть следующее:

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeInType            #-}
{-# LANGUAGE TypeFamilies          #-}

import Data.Kind

data Typey (s :: c) = Marker

class Character c where
  showVal :: Typey (s :: c a) -> a -> ShowS

class Character (Letter l) => Alphabet l where
  data family Letter l :: * -> *

data Symbol l (a :: Letter l s) where
  Terminal :: (Alphabet l) => s -> Symbol l (a :: Letter l s)

instance (Alphabet l) => Show (Symbol l a) where
  showsPrec d (Terminal val) = showVal (Marker :: Typey a) val

-- Example language
data ExampleLanguage = ExampleLanguage

instance Alphabet ExampleLanguage where
  data Letter ExampleLanguage a where
    Variable :: Letter ExampleLanguage String
    Comment :: Letter ExampleLanguage String
    EqualSign :: Letter ExampleLanguage ()
    Deref :: Letter ExampleLanguage ()

instance Character (Letter ExampleLanguage) where
--    showVal (_ :: Typey Variable) = showString
--    showVal (_ :: Typey Comment) = showString
--    showVal (_ :: Typey EqualSign) = const $ showString "="
--    showVal (_ :: Typey Deref) = const $ showString "*"
    showVal _ = const $ showString "error"
test :: Symbol ExampleLanguage Comment
test = Terminal "some comment"

Вы могли видеть, что я начал реализовывать showVal, но здесь у меня возникли проблемы с завершением реализации. Когда я пытаюсь раскомментировать строки в instance Letter (Character ExampleLanguage), компилятор быстро жалуется:

main.hs:40:14: error:
    • Couldn't match type ‘a1’ with ‘()’
      ‘a1’ is a rigid type variable bound by
        the type signature for:
          showVal :: forall k (a :: k) a1 (s :: Character
                                                  ExampleLanguage a1).
                     Typey s -> a1 -> ShowS
        at main.hs:38:5
      Expected type: Typey 'EqualSign
        Actual type: Typey s
    • When checking that the pattern signature: Typey 'EqualSign
        fits the type of its context: Typey s
      In the pattern: _ :: Typey EqualSign
      In an equation for ‘showVal’:
          showVal (_ :: Typey EqualSign) = const $ showString "="
    • Relevant bindings include
        showVal :: Typey s -> a1 -> ShowS (bound at main.hs:38:5)

Я не уверен, что понимаю, на что жалуется компилятор. Из определения Character ExampleLanguage в GADT может быть ясно, что я пытаюсь сопоставить шаблоны разных конструкторов, выводя разные строки в зависимости от буквы.

Как я могу заставить это работать? Формат данных не является фиксированным, вы можете его немного изменить, пока Symbol содержит информацию о типе алфавита, буквы и типа представления буквы.


haskell existential-type gadt
person WorldSEnder    schedule 31.01.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Сопоставление шаблонов в конструкторах GADT, а не в их типах

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE TypeFamilies          #-}

class Character c where
  showVal :: c a -> a -> ShowS

class Character (Letter l) => Alphabet l where
  data family Letter l :: * -> *

-- Example language
data ExampleLanguage = ExampleLanguage

instance Alphabet ExampleLanguage where
  data Letter ExampleLanguage a where
    Variable :: Letter ExampleLanguage String
    Comment :: Letter ExampleLanguage String
    EqualSign :: Letter ExampleLanguage ()
    Deref :: Letter ExampleLanguage ()

instance Character (Letter ExampleLanguage) where
    showVal Variable = showString
    showVal Comment = showString
    showVal EqualSign = const $ showString "="
    showVal Deref = const $ showString "*"

Включите этот тег в Symbol, чтобы позже можно было сопоставить его с образцом.

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE TypeInType            #-}

data Symbol l (a :: Letter l s) where
  Terminal :: Letter l s -> s -> Symbol l (a :: Letter l s)

instance (Alphabet l) => Show (Symbol l a) where
  showsPrec d (Terminal tag val) = showVal tag val

test :: Symbol ExampleLanguage Comment
test = Terminal Comment "some comment"
person Cirdec    schedule 31.01.2018
comment
Я не понимаю, как я мог бы реализовать instance (Alphabet l) => Show (Symbol l a) where с таким подходом. a — это конкретная буква в этом случае, но она находится в информации о типе и не может быть передана в качестве аргумента в showVal, не так ли? - person WorldSEnder; 31.01.2018
comment
За исключением некоторых улучшений в GHC, о которых я не знаю, тип Symbol ExampleLanguage Comment не имеет смысла, поскольку Comment является конструктором GADT и не может быть повышен. - person Cirdec; 31.01.2018
comment
GHC 8 меня удивил. Я добавил, как определить Symbol. - person Cirdec; 01.02.2018
comment
Осталась одна проблема: теперь это допустимо: (Terminal Comment "some comment") :: Symbol ExampleLanguage Variable т.е. если две буквы имеют один и тот же тип, компилятор не уловит, что я ввожу разные буквы в конструктор и тип - person WorldSEnder; 01.02.2018