Тип Family как аргумент для ввода синонима

У меня есть тип данных, который выглядит как

data G f n a where 
  G :: a -> G f n a -> G f (f n) a

Это контейнер, индексированный натуральными числами, который принимает функцию, определяющую, как действовать индуктивно.

Я могу легко определить синоним типа, например

type G' n a = G S n a

Но я хотел бы иметь возможность использовать функцию идентификации.

Я пытался использовать Data.Functor.Identity, но даже при переопределении с помощью PolyKinds я не могу получить функцию уровня типа для Naturals (:k Identity => Nat -> Nat), поэтому я обратился к семействам типов, определив

type family Id a where 
  Id a = a

который, круто, компилируется. К сожалению, я ввожу type G'' n a = G Id n a и получаю сообщение об ошибке

The type family ‘Id’ should have 1 argument, but has been given none
In the type synonym declaration for ‘G''’

Итак, есть ли способ использовать семейство типов в синонимах типов? Это кажется идеальным конечным состоянием.

(Расширения, которые я сейчас использую, это {-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeInType, PolyKinds #-})


haskell dependent-type type-families
person Eliza Brandt    schedule 23.05.2018    source источник

Ответы (1)


arrow_upward
14
arrow_downward

Вы не можете передавать семейства типов (или синонимы типов) в обход ненасыщенных, но вы можете передавать токен, который представляет это семейство типов. Затем, когда пришло время применить семейство типов к аргументу, вы можете найти токен, который вам дали.

type family Apply (token :: *) (n :: Nat) :: Nat

data G token n a where
    G :: a -> G token n a -> G token (Apply token n) a

Теперь вы можете определить токены и как их применять.

data SToken
type instance Apply SToken n = S n

data IdToken
type instance Apply IdToken n = n

И ваши синонимы:

type G' = G SToken
type GId = G IdToken

Этот трюк — обход представлений функций, а не самих функций — называется дефункционализацией и был первоначально разработанный в 70-х как метод реализации для языков функционального программирования более высокого порядка. (Кстати, эта газета потрясающе читается.)

Я не знаю, единственный ли это способ сделать то, что вы хотите, но singletons примерно так и делает. Дополнительная информация в singletons блоге автора.

person Benjamin Hodgson♦    schedule 23.05.2018