Описание тега singleton-type

None Одинокий тип, особенно в контексте программирования с зависимой типизацией в таких языках, как Haskell и Scala. По вопросам о шаблоне проектирования singleton в объектно-ориентированном программировании используйте [singleton].
1 ответ

Работа с доказательствами с участием CmpNat и синглетонов в Haskell

Я пытаюсь создать некоторые функции для работы со следующим типом. В следующем коде используются библиотеки синглетонов и ограничений на GHC-8.4.1: {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LAN…
1 ответ

Как создать объект Birt Runtime как синглтон весной

Я хочу создать одноэлементный объект birt, поскольку объект birt - это объект с большим весом, я новичок в этой технологии, поэтому любая помощь будет полезна.
22 июл '14 в 06:49
0 ответов

Сжатие типов и значений вместе без экспоненциального увеличения

Предположим, у меня есть пара структур данных; один представляет тип, а другой значение: data Schema = Leaf | PairOf Schema Schema | ListOf Schema data ValueOf (schema :: Schema) where LeafElem :: String -> ValueOf 'Leaf PairElem :: ValueOf x -&g…
2 ответа

Можно ли составить размерный список, используя одноэлементные Натс (например, 0, 1, ...) из списков в Haskell?

Узнав о синглетонах и (полу) зависимой типизации, я начал пытаться составить список размеров из обычного списка на Haskell с размерами, заданными Натсом, такими как 0, 1, 2, 3,... вместо Z, S Z, S (S Z) и т. Д. Я использую библиотеку Data.Singletons…
2 ответа

Получить экземпляр синглтон-типа в Scala

Я хочу получить экземпляр типа Singleton в Scala, это возможно? Пример: (я знаю, что в этом случае это можно сделать проще) sealed trait Animal case object Dog extends Animal case object Cat extends Animal trait Person { def name: String // Is there…
20 фев '19 в 12:10
1 ответ

Где поставить неявное значение, чтобы включить неявное преобразование типа синглтон

Рассмотрим случай: class T[A0, B0](val a: A0, val b: B0) class A class B(val a: A) { b => implicit def t: T[a.type, b.type] = new T(a, b) } val b = new B(new A) val t1 = implicitly[T[b.a.type, b.type]]// can't compile, I want t1 = b.t Как включит…
29 дек '16 в 07:39
1 ответ

Функция репликации для списка с индексом длины с использованием GHC.TypeLits и синглетонов

Я пытаюсь написать функцию репликации для индексации по длине списка, используя механизм из GHC.TypeLits, синглтонов и ограничений. Vect тип и подпись для replicateVec приведены ниже: data Vect :: Nat -> Type -> Type where VNil :: Vect 0 a VCo…
07 апр '18 в 15:49
1 ответ

Удивительные эквивалентности и неэквивалентности относительно этого типа

Похоже, имеет значение, обращаетесь ли вы к this.type изнутри черты или из области, в которой создается объект, с удивительными результатами. import scala.reflect.runtime.universe._ trait Trait { val ttag = typeOf[this.type] println(s"Trait construc…
2 ответа

Явные несоответствия в одноэлементных типах

У меня есть пара вопросов о синглтон-типах, но, поскольку они оба очень тесно связаны, я публикую их в одной теме. Q1. Почему #1 не компилируется, а #2 -? def id(x: Any): x.type = x // #1 def id(x: AnyRef): x.type = x // #2 Q2. Тип правильно выведен…
2 ответа

Singletons TypeRepStar Sing Экземпляр данных

Я новичок в Haskell, так что, возможно, я упускаю что-то очевидное, но в чем здесь проблема? Библиотека синглетонов обеспечивает Sing экземпляр для вида * в import Data.Singletons.TypeRepStar, Sing Семейство данных определяется следующим образом. da…
11 авг '17 в 19:47
1 ответ

Проблемы с типом данных и синглетонами в Haskell

Я пытаюсь построить программу для синтаксического анализа регулярных выражений с использованием библиотеки GADTs и синглетонов Я получаю странное сообщение об ошибке: Couldn't match type ‘Integer’ with ‘Nat’ Expected type: DemoteRep 'KProxy Actual t…
14 апр '16 в 13:46
2 ответа

Какой тип: соответствует m s = m == fromSing s?

Используя библиотеку синглетонов, эта простая функция компилируется и работает. Но ghci и ghc расходятся во мнениях относительно его сигнатуры, и если любое из их предложений будет вставлено в код, компиляция не удастся. Какой тип подписи будет прин…
28 мар '16 в 05:32
2 ответа

Scala: есть ли способ создания встроенных типов?

По сути, я хотел бы иметь возможность написать что-то вроде этого: val x :('k1.type, Int) = 'k1 -> 1 val y :('k2.type, Int) = 'k2 -> 2 Где типы x и y несовместимы, но либо совместно используют супер тип, либо могут быть аннотированы границами …
03 дек '14 в 13:56
2 ответа

Синглтоны в гетерогенных списках

Я хотел бы написать функцию, которая анализирует гетерогенный список. Ради аргумента, давайте иметь следующее data Rec rs where Nil :: Rec '[] Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs ) class Analyze name ty where analyze :: Proxy name …
1 ответ

Не удается доказать, что одноэлементные типы являются одноэлементными типами при создании экземпляра класса типов

Предположим, у меня есть класс типов, который доказывает, что все типы в Shapeless coproduct являются одноэлементными типами: import shapeless._ trait AllSingletons[A, C <: Coproduct] { def values: List[A] } object AllSingletons { implicit def cn…
14 сен '14 в 21:58
1 ответ

Доказательство неравенства типа в GHC

В образовательных целях я пытался восстановить пример из книги "Разработка на основе типов с Idris" (а именно RemoveElem.idr) в Haskell, используя различные языковые расширения и синглтон-типы. Суть его состоит в том, что функция удаляет элемент из …
1 ответ

Использование идиоматического логического равенства (синглтоны)

Я хочу создать структуру данных для хранения элементов, помеченных на уровне типа с помощью Symbol. Это: data Store e (ss :: [Symbol]) where Nil :: Store e '[] Cons :: e s -> Store e ss -> Store e (s ': ss) data HasElem (a :: k) (as :: [k]) wh…
10 июл '16 в 08:29
2 ответа

Ограничение типов, которые может принимать параметр типа в объявлениях данных

Я знаю, что в Haskell есть параматизированные типы данных: data Maybe a = Nothing | Just a Но есть ли способ ограничить вид типов, которые a можно обозначить? В частности, я хотел бы создать тип data Tag a = Tag a такой, что a можно взять либо тип T…
12 май '16 в 01:39
1 ответ

Синоним шаблона связывается не так, как обычный шаблон

Функция f не проверяет тип в следующем коде, который использует синглтоны с Frames и Vinyl: f :: forall rs1 rs2. SList rs1 -> Frame (Record rs1) -> Int f (OnlyRecord s1 t1) df1 = broadcast (*) (rhead <$> df1) pattern OnlyRecord :: Sing s…
30 ноя '17 в 02:04
2 ответа

Используя синглеты haskell, как я могу написать `fromList:: [a] -> Vec a n`?

Как часть моего путешествия в понимании singletons Я попытался преодолеть разрыв между безопасностью времени компиляции и повышением значений времени выполнения в безопасности этого зависимого типа. Хотя я думаю, что минимальным примером значений "в…