Синглтоны TypeRepStar Sing Data Instance

Я новичок в Haskell, поэтому я, вероятно, упускаю что-то очевидное, но в чем здесь проблема?

Библиотека singletons предоставляет экземпляр Sing для вида * в import Data.Singletons.TypeRepStar.

Семейство данных Sing определяется следующим образом.

data family Sing (a :: k)

и экземпляр * определяется как..

data instance Sing (a :: *) where
  STypeRep :: Typeable a => Sing a

Я пытаюсь воспроизвести минимальную версию этого, используя следующее...

{-# LANGUAGE GADTs
           , TypeFamilies
           , PolyKinds
           #-}

module Main where

import Data.Typeable

data family Bloop (a :: k)
data instance Bloop (a :: *) where
  Blop :: Typeable a => Bloop a

main :: IO ()
main = putStrLn "Hello, Haskell!"

Но я получаю следующую ошибку...

Main.hs:12:3: error:
    • Data constructor ‘Blop’ returns type ‘Bloop a’
         instead of an instance of its parent type ‘Bloop a’
    • In the definition of data constructor ‘Blop’
         In the data instance declaration for ‘Bloop’
    |
 12 |   Blop :: Typeable a => Bloop a
    |   ^

singleton-type haskell
person pat    schedule 11.08.2017    source источник
comment
никогда не думал, что увижу, что я новичок в хаскеле и синглтонах в одном посте   -  person Justin L.    schedule 14.08.2017
comment
@ДжастинЛ. У меня большой опыт метапрограммирования на C++, так что для меня это не так страшно :D   -  person pat    schedule 14.08.2017

Ответы (2)


arrow_upward
5
arrow_downward

Компилятор настаивает на том, что a в Bloop (a :: *) и a в Typeable a => Bloop a не являются одним и тем же a. Точно такую ​​же ошибку выдает, если заменить один из них на b:

data instance Bloop (b :: *) where
      Blop :: Typeable a => Bloop a

* Data constructor `Blop' returns type `Bloop a'
    instead of an instance of its parent type `Bloop b'
* In the definition of data constructor `Blop'
  In the data instance declaration for `Bloop'

Это можно сделать более заметным с помощью -fprint-explicit-kinds:

* Data constructor `Blop' returns type `Bloop k a'
    instead of an instance of its parent type `Bloop * a'
* In the definition of data constructor `Blop'
  In the data instance declaration for `Bloop'

Теперь мы можем ясно видеть прямо в сообщении об ошибке, что один a имеет тип k, а другой тип *. Отсюда очевидно решение — явно объявить вид второго a :

data instance Bloop (a :: *) where
      Blop :: Typeable (a :: *) => Bloop (a :: *)  -- Works now

Похоже, это происходит из-за расширения PolyKinds. Без него предполагается, что второе a имеет вид *, и, таким образом, исходное определение работает.

person Fyodor Soikin    schedule 11.08.2017

arrow_upward
2
arrow_downward

Похоже, что расширение PolyKinds вызывает ошибку. Библиотека singletons разделяет объявление data family и определения data instance на разные файлы. Для работы семейства данных требуется расширение PolyKinds, но если экземпляр выйдет из строя, если расширение включено. Кажется, вместо этого вы должны использовать расширение KindSignatures.

Def.hs

{-# LANGUAGE PolyKinds, TypeFamilies #-}

module Def (Bloop) where

data family Bloop (a :: k)

Main.hs

{-# LANGUAGE GADTs
           , TypeFamilies
           , KindSignatures
           #-}

module Main where

import Def
import Data.Typeable

data instance Bloop (a :: *) where
  Blop :: Typeable a => Bloop a

main :: IO ()
main = putStrLn "Hello, Haskell!"
person pat    schedule 11.08.2017