Введите семейство в качестве аргумента для ввода синонима - PullRequest
Новая
       44

Введите семейство в качестве аргумента для ввода синонима

0 голосов
/ 23 мая 2018

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

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 #-})

1 Ответ

0 голосов
/ 23 мая 2018

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

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

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

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

...