Ограничения равенства в экземплярах типов

Допустим, у меня есть следующее:

type family TF a b

Могу ли я написать что-то вроде этого

type instance TF Int t = (t ~ (x,y)) => (Int,x,y)

как возможно глупый пример.

Этот вопрос соответствует той же теме, что и принятый ответ на этот вопрос: Haskell: ограничение равенства в экземпляре < /а>

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


haskell type-families
person Clinton    schedule 15.02.2016    source источник
comment
Думаю, нет, так как x,y не входит в область действия. Как написано, это по существу будет включать экзистенциальные типы, которые не являются первоклассными в Haskell.   -  person chi    schedule 15.02.2016
comment
type family Fst x where Fst (x,y) = x; type family Snd x where Snd (x,y) = y; type instance TF Int t = (Int, Fst t, Snd t). Проще всего дать вашему индексу одно закрытое семейство, которое сокращается только для пар: type instance TF Int x = TF_Int x; type family TF_Int x where TF_Int (x,y) = (Int, x, y).   -  person user2407038    schedule 15.02.2016
comment
@user2407038 user2407038, я считаю, что подход Fst/Snd более ленивый и, следовательно, позволит более полезные сокращения.   -  person dfeuer    schedule 16.02.2016

Ответы (1)


arrow_upward
4
arrow_downward

Возможно, вы сможете сделать это в GHC 8.0, используя новый TypeError, в зависимости от того, что вы подразумеваете под "заставить второй аргумент быть парой".

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

module Pair where

import GHC.TypeLits

type family Fst p where
  Fst (x, y) = x
  Fst _t = TypeError (Text "Fst: expected a pair, but got " :<>: ShowType _t)

type family Snd p where
  Snd (x, y) = y
  Snd _t = TypeError (Text "Snd: expected a pair, but got " :<>: ShowType _t)

type family TF a b
type instance TF Int t = (Int, Fst t, Snd t)

Теперь вы должны получить ошибку компиляции, если попытаетесь применить TF Int к не-кортежу:

*Pair> let x = x in x :: TF Int Bool

<interactive>:9:1: error:
    • Fst: expected a pair, but got Bool
    • When checking the inferred type
        it :: (Int, (TypeError ...), (TypeError ...))

Однако на самом деле это не «заставляет» аргумент быть парой больше, чем вызов fromJust «принуждает» его аргумент иметь форму Just x. Это действительно программирование с частичными функциями на уровне типа.

Корректность приложений семейства типов полностью определяется видом семейства типов, и пара (x, y) имеет тот же тип *, что и, скажем, Bool. Вы не можете волшебным образом навлечь на себя ограничение, просто написав приложение семейства типов. Если вы хотите получить ограничение на уровне типа, вы должны написать его слева от =>.

В связанном вопросе CanFilter (b -> c) a уже является ограничением, поэтому оно может подразумевать b ~ c.

person Reid Barton    schedule 15.02.2016
comment
Это действительно программирование с частичными функциями на уровне типа. Я не думаю, что здесь это точно так - это было бы более верно без случая TypeError. В этом случае вы получите TF Int Bool ~ (Int, Fst Bool, Snd Bool) — последние два типа застряли (т. е. их нельзя никогда уменьшить), но они не выдают ошибку типа. Но Fst Bool до сих пор обитает на дне! Суть TypeError в том, что если оно когда-либо появляется в типе, это действительно ошибка типа. Fst Bool с TypeError не обитает снизу — потому что самого типа просто не существует. - person user2407038; 16.02.2016
comment
Я не понимаю. Если у меня нет случая TypeError, то всего Fst; Fst Int - застрявший тип, как вы говорите. Цель TypeError состоит в том, чтобы сделать Fst Int ошибкой, поэтому Fst становится частичным. - person Reid Barton; 16.02.2016