Возможны ли доказательства экземпляров семейства типов?

Во-первых, я начал с некоторых типичных натуральных чисел на уровне типов.

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

Итак, я хотел создать тип данных, представляющий n-мерную сетку. (Обобщение того, что можно найти на Оценка клеточных автоматов комонадна .)

data U (n :: Nat) x where
  Point     :: x                           -> U Z     x
  Dimension :: [U n x] -> U n x -> [U n x] -> U (S n) x

Идея состоит в том, что тип U num x - это тип num-мерной сетки x, которая "сфокусирована" на определенной точке в сетке.

Итак, я хотел сделать это комонадой и заметил, что есть потенциально полезная функция, которую я могу сделать:

ufold :: (x -> U m r) -> U n x -> U (Plus n m) r
ufold f (Point x) = f x
ufold f (Dimension ls mid rs) =
  Dimension (map (ufold f) ls) (ufold f mid) (map (ufold f) rs)

Теперь мы можем реализовать «соединение измерений», которое превращает n-мерную сетку m-мерных сеток в (n + m) -мерную сетку в терминах этого комбинатора. Это пригодится при работе с результатом cojoin, который будет создавать сетки сеток.

dimJoin :: U n (U m x) -> U (Plus n m) x
dimJoin = ufold id

Все идет нормально. Я также заметил, что экземпляр Functor можно записать в терминах ufold.

instance Functor (U n) where
  fmap f = ufold (\x -> Point (f x))

Однако это приводит к ошибке типа.

Couldn't match type `n' with `Plus n 'Z'

Но если мы сделаем копию макаронных изделий, ошибка типа исчезнет.

instance Functor (U n) where
  fmap f (Point x) = Point (f x)
  fmap f (Dimension ls mid rs) =
    Dimension (map (fmap f) ls) (fmap f mid) (map (fmap f) rs)

Я ненавижу вкус копировальной пасты, поэтому мой вопрос такой. Как определить системе типов, что Plus n Z равно n? И загвоздка в следующем: вы не можете внести изменения в экземпляры семейства типов, которые заставили бы dimJoin выдать аналогичную ошибку типа.


haskell type-level-computation type-families
person Dan Burton    schedule 18.10.2012    source источник
comment
Помогает ли размещение Plus n Z ~ n в контексте экземпляра Functor? Вам просто нужно воспроизвести это ограничение, пока n не станет мономорфным.   -  person Ptharien's Flame    schedule 18.10.2012

Ответы (1)


arrow_upward
5
arrow_downward

Что вам нужно, так это хороший пропозициональный тип равенства:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

data Nat = Z | S Nat

type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus Z m = m
type instance Plus (S n) m = S (Plus n m)

data (:=) :: k -> k -> * where
  Refl :: a := a

data Natural (n :: Nat) where
  Zero :: Natural Z
  Suc  :: Natural n -> Natural (S n)

plusZero :: Natural n -> n := (n `Plus` Z)
plusZero Zero = Refl
plusZero (Suc n) | Refl <- plusZero n = Refl

Это позволяет вам доказывать произвольные вещи о ваших типах и применять эти знания в области видимости локально путем сопоставления с образцом на Refl.

Одна неприятная вещь заключается в том, что мое plusZero доказательство требует индукции по рассматриваемому естественному виду, что вы не сможете сделать по умолчанию (поскольку оно не существует во время выполнения). Однако класс типов для генерации Natural свидетелей было бы несложно.

Другой вариант для вашего конкретного случая может заключаться в том, чтобы просто инвертировать аргументы в плюс в определении вашего типа, чтобы вы получили Z слева, и он автоматически уменьшится. Часто хороший первый шаг - убедиться, что ваши типы настолько просты, насколько вы можете их создать, но тогда вам часто понадобится пропозициональное равенство для более сложных вещей, несмотря ни на что.

person copumpkin    schedule 19.10.2012
comment
Кстати, в GHC 7.6 варсимы теперь являются конструкторами типа конструкторы. Так что вы могли бы назвать равенство (==), если хотите. - person Andy Morris; 25.10.2012
comment
Я попытался создать экземпляр отношения эквивалентности с Refl Z Z, но произошла следующая ошибка. Как создать значение, обеспечивающее свойство Reflexive? ‹Br› Не удалось сопоставить ожидаемый тип «Nat -› Nat - ›t» с фактическим типом «EqProp a0 a0» ‹br› Соответствующие привязки включают его :: t (привязано на ‹interactive›: 71: 1) ‹br› Функция «Refl» применяется к двум аргументам, ‹br›, но ее тип «EqProp a0 a0» не имеет никакого ‹br› В выражении: Refl ZZ ‹br› В уравнении для «it»: it = Refl ZZ - person jackb; 01.12.2015