Можно ли получить тип типового конструктора в Haskell?

Я работаю с Data.Typeable и, в частности, хочу иметь возможность генерировать правильные типы определенного типа (скажем *). Проблема, с которой я сталкиваюсь, заключается в том, что TypeRep позволяет нам выполнить следующее (работа с версией в GHC 7.8):

let maybeType = typeRep (Proxy :: Proxy Maybe)
let maybeCon = fst (splitTyConApp maybeType)
let badType = mkTyConApp maybeCon [maybeType]

Здесь badType является в некотором смысле представлением типа Maybe Maybe, который не является допустимым типом любого вида:

> :k Maybe (Maybe)

<interactive>:1:8:
    Expecting one more argument to ‘Maybe’
    The first argument of ‘Maybe’ should have kind ‘*’,
      but ‘Maybe’ has kind ‘* -> *’
    In a type in a GHCi command: Maybe (Maybe)

Я не ищу, чтобы это выполнялось на уровне типа, но я хотел бы написать программу, которая достаточно умна, чтобы избежать создания таких типов во время выполнения. Я могу сделать это с помощью уровней данных на уровне TypeRep. В идеале у меня было бы что-то вроде

data KindRep = Star | KFun KindRep KindRep

и иметь функцию kindOf с kindOf Int = Star (возможно, действительно kindOf (Proxy :: Proxy Int) = Star) и kindOf Maybe = KFun Star Star, чтобы я мог "добросердечно проверить" значение TypeRep.

Я думаю, что могу сделать это вручную с помощью поликидного типа, например Typeable, но я бы предпочел не писать собственные экземпляры для всего. Я также предпочел бы не возвращаться к GHC 7.6 и использовать тот факт, что существуют отдельные классы типов для типов Typeable различных типов. Я открыт для методов, которые получают эту информацию от GHC.

Ответы

Ответ 1

Мы можем получить тип типа, но для этого нам нужно бросить целый набор расширений языка в GHC, включая (в данном случае) более сомнительные UndecidableInstances и AllowAmbiguousTypes.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Proxy

Используя ваше определение для KindRep

data KindRep = Star | KFun KindRep KindRep

мы определяем класс Kindable вещей, чей вид может быть определен

class Kindable x where
    kindOf :: p x -> KindRep

Первый пример для этого прост, все из рода * равно Kindable:

instance Kindable (a :: *) where
    kindOf _ = Star

Получение типа более высокого сорта затруднено. Мы попытаемся сказать, что если мы сможем найти вид своего аргумента и вид результата применения его к аргументу, мы сможем выяснить его вид. К сожалению, поскольку у него нет аргумента, мы не знаем, какой тип будет его аргументом; поэтому нам нужно AllowAmbiguousTypes.

instance (Kindable a, Kindable (f a)) => Kindable f where
    kindOf _ = KFun (kindOf (Proxy :: Proxy a)) (kindOf (Proxy :: Proxy (f a)))

В сочетании, эти определения позволяют нам писать такие вещи, как

 kindOf (Proxy :: Proxy Int)    = Star
 kindOf (Proxy :: Proxy Maybe)  = KFun Star Star
 kindOf (Proxy :: Proxy (,))    = KFun Star (KFun Star Star)
 kindOf (Proxy :: Proxy StateT) = KFun Star (KFun (KFun Star Star) (KFun Star Star))

Просто не пытайтесь определить тип поликидного типа, например Proxy

 kindOf (Proxy :: Proxy Proxy)

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