Как можно назвать семейство типов как функцию рода более высокого порядка? - PullRequest
Новая
       8

Как можно назвать семейство типов как функцию рода более высокого порядка?

0 голосов
/ 06 декабря 2018

Можно ли использовать семейство типов в качестве «функции типа» высшего порядка для передачи другому семейству типов?Простым примером будет следующий код: 

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
import GHC.TypeLits as T

type family Apply (f :: Nat -> Nat -> Nat) (n :: Nat) (m :: Nat) :: Nat where
  Apply f n m = f n m

type family Plus (n :: Nat) (m :: Nat) :: Nat where
  Plus n m = n T.+ m

type family Plus' (n :: Nat) (m :: Nat) :: Nat where
  Plus' n m = Apply (T.+) n m

Первое объявление Plus допустимо, а второе (Plus') выдает следующую ошибку: 

Test.hs:19:3: error:
    • The type family ‘+’ should have 2 arguments, but has been given none
    • In the equations for closed type family ‘Plus'’
      In the type family declaration for ‘Plus'’
   |
19 |   Plus' n m = Apply (T.+) n m
   |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^

Есть ли способ использовать функцию типа Apply для реализации Plus?

РЕДАКТИРОВАТЬ Комментатор, связанный с отчетом запроса функции в https://ghc.haskell.org/trac/ghc/ticket/9898. В нем упоминаетсяsingleton библиотека.Я был бы счастлив с примером использования этого или других «обходных путей» для достижения подобного эффекта абстрагирования по арифметическим операциям на Nat, таких как +, *, - и Mod.

1 Ответ

0 голосов
/ 07 декабря 2018

Полезным подходом является нефункционализация.Вы можете реализовать его самостоятельно или найти реализацию в библиотеке singletons.

Ядро является «открытым видом»: 

data TYFUN :: Type -> Type -> Type
type TyFun a b = TYFUN a b -> Type

TyFun a b - открытый вид;он не закрыт как нормальный, продвинутый, data вид.Вы «объявляете» новые функции следующим образом. 

data Plus :: TyFun Nat (TyFun Nat Nat)

Затем вы можете определить это семейство типов, чтобы связать объявление и определение 

type family Apply (f :: TyFun a b) (x :: a) :: b
data PlusSym1 :: Nat -> TyFun Nat Nat -- see how we curry
type instance Apply Plus x = PlusSym1 x
type instance Apply (PlusSym1 x) y = x + y

Теперь, Plus - это обычный конструктор типов:тип данных, а не семейство типов.Это означает, что вам разрешено передавать его другим типам семей.Обратите внимание, что они должны быть TyFun осознающими себя. 

type family Foldr (cons :: TyFun a (TyFun b b)) (nil :: b) (xs :: [a]) :: b where
    Foldr _ n '[] = n
    Foldr c n (x:xs) = Apply (Apply c x) (Foldr c n xs)
type Example = Foldr Plus 0 [1,2,3]

Идея открытого вида заключается в том, что Type уже является открытым видом, а такие виды, как A -> Type, A -> B -> Type, сами открыты.,TYFUN - это тег, идентифицирующий вещи как TyFun s, а TyFun - это открытый вид, который эффективно не пересекается с другими открытыми типами.Вы также можете использовать Type открытый вид прямой: 

type family TyFunI :: Type -> Type
type family TyFunO :: Type -> Type
type family Apply (f :: Type) (x :: TyFunI f) :: TyFunO f
data Plus :: Type
data PlusSym1 :: Nat -> Type
type instance TyFunI Plus = Nat
type instance TyFunO Plus = Type
type instance TyFunI (PlusSym1 _) = Nat
type instance TyFunO (PlusSym1 _) = Nat
type instance Apply Plus x = PlusSym1 x
type instance Apply (PlusSym1 x) y = x + y

С положительной стороны, это может обрабатывать функции зависимого типа, но, с другой стороны, это происходит только потому, что он бесстыдно выбрасываетпроверяя все «Type ly-typed».Это не так плохо, как String код с типичной линией, так как это все время компиляции, но все же.

...