Вопросы по теме 'type-level-computation'
Могу ли я статически отклонять различные экземпляры экзистенциального типа?
Первая попытка
Сложно сделать этот вопрос содержательным, но для минимального примера предположим, что у меня есть такой тип:
{-# LANGUAGE GADTs #-}
data Val where
Val :: Eq a => a -> Val
Этот тип позволяет мне с радостью составить...
311 просмотров
schedule
27.10.2021
Экземпляр семейства типов Haskell с ограничениями типа
Я пытаюсь представить выражения с помощью семейств типов, но, похоже, не могу понять, как написать ограничения, которые мне нужны, и я начинаю чувствовать, что это просто невозможно. Вот мой код:
class Evaluable c where
type Return c :: *...
886 просмотров
schedule
25.09.2021
Почему для вычислений на уровне типов требуется техника Aux?
Я почти уверен, что мне здесь чего-то не хватает, так как я новичок в Shapeless и учусь, но когда на самом деле требуется техника Aux ? Я вижу, что он используется, чтобы раскрыть type оператор, подняв его до сигнатуры другого «сопутствующего»...
1511 просмотров
schedule
03.11.2021
Как получить значения уровня типа '[String] в Haskell?
Я могу получить значение уровня типа String следующим образом:
> :set -XDataKinds
> import Data.Proxy
> import GHC.TypeLits
> symbolVal (Proxy :: Proxy "test")
"test"
Как мне получить значения '[String] , например Proxy ::...
984 просмотров
schedule
07.10.2021
Как мне проверить бесформенность, если тип является членом HList?
Я выполняю последовательность шагов предварительной обработки для строк, и я думал об использовании HList s для повышения безопасности моих шагов. Некоторые этапы обработки должны выполняться после других, поэтому я подумал о кодировании их в...
233 просмотров
schedule
01.11.2021
Scala: являются ли операторы типов с ограничениями обобщенного типа?
У меня есть следующая формулировка натуральных чисел Пеано на уровне типа: gist
с типом натурального числа, имеющим следующий интерфейс:
sealed trait NaturalNumber {
type MatchZero[T <: Up, F[_ <: NaturalNumber] <: Up, Up] <:...
65 просмотров
schedule
12.09.2021
Поиск неявного внутри вызова reify (макрос scala)
Мне нужно найти неявное значение в заданной позиции. Я сохранил позицию из предыдущего вызова макроса в классе, например:
class Delayed[+Kind[_[_]]](val sourceFilePath: String, val callSitePoint: Int) {
def find[F[_]]: Kind[F] = macro...
148 просмотров
schedule
16.10.2021
В GHC.TypeLits для чего хорош someNatVal (чего мы не можем сделать с natVal)?
Я пытаюсь понять GHC.TypeLits и конкретно someNatVal . Я понимаю, как это используется в этом блоге опубликовать здесь , но, как уже упоминалось, тот же пример можно было бы реализовать с использованием natVal , например:
isLength ::...
676 просмотров
schedule
23.02.2022
Числа Пеано на уровне типов и неразрешимые экземпляры
Следуя этому руководству , у меня есть следующий код:
{-# LANGUAGE DataKinds, 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)...
131 просмотров
schedule
28.03.2022
Подпись числового типа
Можно ли создать тип с числовым аргументом?
то есть, если я хочу создать тип целых чисел с фиксированной разрядностью:
newtype FixedWidth w = FixedWidth Integer
addFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (w+1)...
158 просмотров
schedule
27.04.2022
Может ли система типов Haskell обеспечить правильный порядок этапов конвейера данных?
Я создаю множество конвейеров обработки данных, используя данные масс-спектрометрии, где данные с прибора очищаются, преобразовываются, масштабируются, проверяются и, наконец, анализируются. Я склонен использовать для этого определение рекурсивного...
220 просмотров
schedule
11.05.2022
Agda - разница между аргументами типа слева и справа от двоеточия
Следующее определение компилируется и ведет себя хорошо:
data Eq {lvl} {A : Set lvl} (x : A) : A → Set where
refl : Eq x x
Однако этот не компилируется:
data Eq {lvl} {A : Set lvl} (x : A) (y : A) : Set where
refl : Eq x x
так как...
134 просмотров
schedule
17.05.2022
Последовательность над разнородным списком в Haskell
Рассмотрим следующее определение HList :
infixr 5 :>
data HList (types :: [*]) where
HNil :: HList '[]
(:>) :: a -> HList l -> HList (a:l)
И семейство типов Map для сопоставления списков уровней типов:
type family Map...
212 просмотров
schedule
28.06.2022
Haskell не может вывести равенства типов (или уровня типа), несмотря на явную аннотацию?
Я пытался реализовать дерево Брауна с Haskell, определенное следующим образом:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies...
147 просмотров
schedule
05.07.2022
Общее преобразование / сворачивание / отображение кортежа / hlist, содержащего некоторый F [_]
Недавно я спросил Сопоставить и уменьшить / свернуть HList of scalaz.Validation и получил отличный ответ о том, как преобразовать фиксированный размер кортеж из Va[T] (который является псевдонимом для scalaz.Validation[String, T] ) в...
531 просмотров
schedule
27.07.2022
Набор уровня типа для алгебраического типа данных
Это частично дублирует этот вопрос: Получение подклассов запечатанного признака , но ответ предлагает отражение во время выполнения, которое мне не подходит, и я хотел бы знать, возможно ли это во время компиляции, возможно, с использованием...
271 просмотров
schedule
02.08.2022
Есть ли способ неявно получить экземпляр объекта
Мы хотим создать кодировщик для произвольного Enumerations с бескаркасным , который в основном создает двунаправленное сопоставление из произвольное число от Enumeration до Byte . В настоящее время наше далеко не оптимальное решение состоит в...
403 просмотров
schedule
09.08.2022
Как вызвать ошибку соответствия шаблону семейства типов в Haskell?
Может ли Haskell указать ошибку соответствия семейства типов? Например, используя закрытое семейство типов:
type family Testf a where
Testf Char = IO ()
Testf String = IO ()
Тип Testf Int — это просто Testf Int . Компилятор не...
314 просмотров
schedule
13.08.2022
Как правильно использовать неоднозначные имплициты для отрицания типа в Scala
В конечном итоге я хочу предоставить одну реализацию класса типа для определенного типа T и другую реализацию для всех других типов, которые не являются T . Я думал (возможно, неправильно), что самый простой способ сделать это — попробовать...
239 просмотров
schedule
13.08.2022
Среда уровня типа в Haskell
Я пытаюсь использовать некоторые расширения Haskell для реализации простого DSL. Я бы хотел, чтобы у переменных был контекст уровня типа. Я знаю, что подобные вещи обычно встречаются в таких языках, как агда или идрис. Но я хотел бы знать, можно ли...
361 просмотров
schedule
07.09.2022
