Блог

Главная - Вопросы по программированию - Мономорфизация с семействами типов

Мономорфизация с семействами типов

#haskell #ghc

#хаскелл #ghc

Вопрос:

Следующий код компилируется, но только с явной сигнатурой типа в bar :

 {-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

type family ResultOf a where
  ResultOf (a -> b) = ResultOf b
  ResultOf a = a

wrap :: (Monad rnd, ResultOf bnch ~ rnd Int) => bnch -> rnd Int
wrap = undefined

foo :: (Monad m) => m Int
foo = undefined

bar :: forall rnd . (Monad rnd, ResultOf (rnd Int) ~ rnd Int) => rnd Int
bar = wrap (foo :: rnd Int)

Я примерно понимаю, почему требуется подпись типа: foo является полиморфной, и GHC не может сказать, что единственный способ ResultOf (forall m . (MonadRandom m) => m Int) ~ rnd Int — это создать экземпляр m at rnd . Я бы хотел, чтобы это было правдой, чтобы GHC мономорфизировал ‘foo` с правильной монадой без явной подписи типа. Есть ли какой-нибудь способ убедить GHC в этом?

Комментарии:

1. Одним из решений является использование newtype в качестве выходных данных функции, чтобы семейство типов не перекрывалось (т. Е. Могло существовать как открытое семейство). Можно ли это сделать без глупой оболочки, которая просто продолжается и сразу же возвращается?

2. У вас есть реальная реализация для wrap ? Мне кажется, что эта функция населена только const ... (и, конечно, различными днищами). ResultOf a ~ a утверждает, что a это не тип функции, потому что это не может быть правдой, если первый шаблон когда-либо совпадал, но он не содержит доказательства этого — вы должны построить это самостоятельно. Обычно способ сделать это — написать GADT, моделирующий доказательство, и иметь класс типа, который неявно создает значения этого доказательства.

3. @user2407038 wrap использует простой класс типов (не показан, поскольку он не имеет отношения к проблеме вывода) для случайной генерации аргументов функции, очень похожих на тестируемый класс QuickCheck.