Edit: Вот действительно простой пример. Мотивация для этого примера ниже.
Это компилирует:
{-# LANGUAGE TypeFamilies #-}
type family F a b
f :: a -> F a b
f = undefined
f' [a] = f a
И ghci сообщает, что:
*Main> :t f'
f' :: [a] -> F a b
Но если мы добавим эту подпись типа в файл выше, он пожалуется:
*Main> :r
[1 of 1] Compiling Main ( test.hs, interpreted )
test.hs:9:14:
Couldn't match type `F a b0' with `F a b'
NB: `F' is a type function, and may not be injective
In the return type of a call of `f'
In the expression: f a
In an equation for `f'': f' [a] = f a
Failed, modules loaded: none.
Что дает?
Мотивация:
После просмотра ] этот вопрос , я подумал, что буду умником и напишу небольшое решение для шутки. План атаки состоит в том, чтобы начать с чисел уровня типа (как обычно), а затем написать небольшую функцию уровня типа Args nac
, которая дает тип функции, который принимает n
копий a
и дает c
. Затем мы можем написать небольшой класс типов для различных n
и продолжить свой путь. Вот что я хочу написать:
{-# LANGUAGE TypeFamilies #-}
data Z = Z
data S a = S a
type family Args n a c
type instance Args Z a c = c
type instance Args (S n) a c = a -> Args n a c
class OnAll n where
onAll :: n -> (b -> a) -> Args n a c -> Args n b c
instance OnAll Z where
onAll Z f c = c
instance OnAll n => OnAll (S n) where
onAll (S n) f g b = onAll n f (g (f b))
Я был удивлен, обнаружив, что это не проверка типов!