Обеспечение параметричности аргументов

Question

Используя RankNTypes, можно применять различные виды параметризации. Например, A id :: A:

newtype A = A { unA :: forall a. a -> a }

Но как насчет случаев, когда мы только заботимся о параметричности функции по ее аргументу? Для конкретного типа случая c будет работать следующее:

newtype X b = X { unX :: forall a. a -> (a, b) }

Например, X (\a -> (a, ())) :: X ().

Я хотел бы понять, как (и можно ли) создать тест параметричности, который работает в более общем плане для функций вида \a -> (a, f a), где f может быть постоянным (как указано выше) или потенциально параметризованным c. Этого нельзя добиться с помощью X. Например, X (\a -> (a, id a)) - ошибка типа. Можно ли это сделать?

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

type PState i o a = i -> (a, o)

Предположим также, что мы заинтересованы в статическом обеспечении того, чтобы a в произвольном m :: PState i o a никоим образом не зависело от i. Другими словами, возможно ли определить функцию f так, чтобы f m был хорошо типизирован, когда значение m не зависит от ввода (и в этом случае оценивается как m) и является в противном случае неправильно набран?

Answer 1

Вам нужно будет создать явную функцию уровня типа для sh этого. Обычно квантифицированные Type -> Type переменные фактически считаются конструкторами типов (инъективными функциями), чего здесь недостаточно. Но могут быть и неинъективные, они просто называются типами семействами . Обратной стороной этого является то, что вам нужны отдельные средства индексации , которые вы хотите, потому что без этого не будет работать вывод типов.

{-# LANGUAGE TypeFamilies, KindSignatures, EmptyDataDecls, TypeInType
           , RankNTypes, UnicodeSyntax #-}

import Data.Kind

type family MyTyFun (f :: Type) (a :: Type) :: Type

newtype GState f = GState { unGS :: ∀ a . a -> (a, MyTyFun f a) }

data Af
type instance MyTyFun Af a = ()
type A = GState Af

data Xf b
type instance MyTyFun (Xf b) a = b
type X b = GState (Xf b)

data Wf
type instance MyTyFun Wf a = a
type W = GState Wf

> unGS (GState (\a -> (a, a)) :: W) 4
(4,4)