Кодирование ограничения уровня типа

Итак, у меня есть конструктор данных, который я использую только на уровне типа, который содержит 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 не продвигается.

Любая помощь приветствуется!

Доставляет ли SomeNat вас туда, куда вам нужно?

Daniel Wagner 17.03.2022 18:08

@DanielWagner Это перемещает непродвигаемую контекстную ошибку в семейства типов GetA и GetB. Так что к сожалению нет :(

CryptoNoob 17.03.2022 18:30
Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
2
2
124
1
Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

Я не уверен, что полностью понимаю, что вам нужно, но если вы хотите сохранить ограничение 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 и в любом случае выполнить его ограничения.

Другие вопросы по теме