Итак, у меня есть конструктор данных, который я использую только на уровне типа, который содержит Nat
. Обычно, если я передаю это на уровне типа и хочу отразить Nat
на уровне термина, мне нужно ограничение KnownNat
. Что я хочу сделать, так это закодировать это ограничение KnownNat
в самом типе, поэтому, если этот тип встречается в сигнатуре где-то, ограничение KnownNat
выводится в теле функции. Это означает, что мне больше не нужно писать ограничение KnownNat
на сайтах использования. Мне нужно только убедиться, что ограничение KnownNat
соблюдается при строительстве.
Я подумал использовать для этого GADT и зашел так далеко:
data Foo = Foo Nat Nat
type family GetA (f :: Foo) :: Nat where
GetA ('Foo a _) = a
type family GetB (f :: Foo) :: Nat where
GetB ('Foo _ b) = b
data KnownFoo (f :: Foo) where
KnownFoo :: (KnownNat (GetA f), KnownNat (GetB f)) => KnownFoo f
foo :: forall (f :: Foo) (kf :: KnownFoo f). Proxy kf -> Integer
foo _ = natVal $ Proxy @(GetA f)
Но это не работает, так как средство проверки типов не понимает, что GetA f
является KnownNat
, хотя передается KnownFoo
. Есть ли способ заставить что-то подобное работать?
Я также попытался полностью переместить f :: Foo
в ограничение KnownFoo
следующим образом:
data Foo = Foo Nat Nat
type family GetA (f :: Foo) :: Nat where
GetA ('Foo a _) = a
type family GetB (f :: Foo) :: Nat where
GetB ('Foo _ b) = b
data KnownFoo where
KnownFoo :: forall f. (KnownNat (GetA f), KnownNat (GetB f)) => Proxy f -> KnownFoo
type family GetFoo (kf :: KnownFoo) :: Foo where
GetFoo ('KnownFoo (Proxy f)) = f
Но тогда у меня нет возможности написать семейство типов GetFoo
, так как оно жалуется, что KnownNat
не продвигается.
Любая помощь приветствуется!
@DanielWagner Это перемещает непродвигаемую контекстную ошибку в семейства типов GetA
и GetB
. Так что к сожалению нет :(
Я не уверен, что полностью понимаю, что вам нужно, но если вы хотите сохранить ограничение KnownNat
, вам нужно будет иметь некоторое представление об этом во время выполнения. Возможно, что-то вроде этого может сработать для вас:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
import GHC.TypeLits
data FooC a b where
FooR :: (KnownNat a, KnownNat b) => FooC a b
type family GetA x where GetA (FooC a b) = a
type family GetB x where GetB (FooC a b) = b
withKnowledge :: FooC a b -> ((KnownNat a, KnownNat b) => r) -> r
withKnowledge FooR r = r
Обратите внимание, что DataKinds
здесь даже нет: мы прямо определяем новый тип, который нам нужен, а не косвенно определяем его пониженную форму. Я думаю, вы можете сделать аналогичный класс Known
для этого.
class KnownFoo f where witness :: f
instance (KnownNat a, KnownNat b) => KnownFoo (FooC a b) where witness = FooR
withKnownFoo :: forall f a b r. (KnownFoo f, f ~ FooC a b) => ((KnownNat (GetA f), KnownNat (GetB f)) => r) -> r
withKnownFoo = withKnowledge (witness @f)
Однако это не кажется супер полезным. В любое время, когда вы можете написать withKnownFoo x
, у вас уже есть соответствующие экземпляры KnownNat
в области видимости, чтобы просто написать x
и в любом случае выполнить его ограничения.
Доставляет ли
SomeNat
вас туда, куда вам нужно?