Вопросы по теме 'existential-type'
Могу ли я статически отклонять различные экземпляры экзистенциального типа?
Первая попытка
Сложно сделать этот вопрос содержательным, но для минимального примера предположим, что у меня есть такой тип:
{-# LANGUAGE GADTs #-}
data Val where
Val :: Eq a => a -> Val
Этот тип позволяет мне с радостью составить...
311 просмотров
schedule
27.10.2021
Почему в GHC Haskell нет экзистенциально количественно определяемых переменных типа
Существуют универсально количественно определяемые типовые переменные и существуют экзистенциально количественно определяемые типы данных. Однако, несмотря на то, что люди иногда используют псевдокод в форме exists a. Int -> a , чтобы помочь...
901 просмотров
schedule
02.10.2021
Перевести / кодировать данные Haskell Obj = forall a. (Показать) = ›Obj a` в Scala
Я не смог придумать, как кодировать Obj в Scala:
{-# LANGUAGE ExistentialQuantification #-}
data Obj = forall a. (Show a) => Obj a
instance Show Obj where show (Obj a) = "Obj " ++ show a
main = print $ show [Obj "hello", Obj 3, Obj True]...
144 просмотров
schedule
21.11.2021
универсальный и экзистенциальный квантификатор в прологе
Как я могу реализовать следующие правила в прологе.
Я пишу фразу «пауки не млекопитающие» как экзистенциальную и универсальную:
¬∃x(mammals(X) ∧ spider(X) ) //It is not the case that mammals are spider
∀X(mammals(X) ⇒ ¬spider(X)) //All mammals...
5298 просмотров
schedule
30.11.2021
Является ли такое использование GADT полностью эквивалентным экзистенциальным типам?
нравится
data Foo = forall a. MkFoo a (a -> Bool)
| Nil
можно легко перевести на GADT:
data Foo where
MkFoo :: a -> (a -> Bool) -> Foo
Nil :: Foo
Есть ли между ними различия: код, который компилируется...
294 просмотров
schedule
03.11.2021
Почему следующий код Scala не компилируется, если не добавлены явные параметры типа?
object Test extends Application {
// compiles:
Map[Int, Value](
0 -> KnownType(classOf[Object]),
1 -> UnknownValue())
// does not compile:
Map(
0 -> KnownType(classOf[Object]),
1 -> UnknownValue())
}
sealed trait...
927 просмотров
schedule
09.03.2022
Являются ли концепции C ++ формой экзистенциального типа?
Я смотрел определение экзистенциальных типов в Википедии ( Existential_types ), и оно похоже на некоторый путь к концепциям в C ++ (особенно к concept lite ).
Являются ли концепции C ++ формой экзистенциального типа?
Если нет, то в чем разница...
2252 просмотров
schedule
10.03.2022
Можно ли заставить переменную экзистенциально квантифицированного типа иметь только один тип?
Рассмотрим следующий код
trait Foo[T] {
def one: Foo[_ >: T]
def two: T
def three(x: T)
}
def test[T](f: Foo[T]) = {
val b = f.one
b.three(b.two)
}
Метод test не может ввести проверку. В нем говорится:
found : (some...
125 просмотров
schedule
12.03.2022
Копия класса case в Scala не всегда работает с экзистенциальным типом `_`
Я пытаюсь copy() класс случая Scala, у которого есть параметр типа. На месте вызова тип значения - Foo[_] .
Это компилируется, как ожидалось:
case class Foo[A](id: String, name: String, v1: Bar[A])
case class Bar[A](v: A)
val foo: Foo[_] =...
75 просмотров
schedule
13.03.2022
Как вернуть универсальный подстановочный знак?
У меня есть псевдоним типа с параметром, и я хотел бы вернуть экземпляры разных типов параметров из метода:
type TC[T] = (ClassTag[T], Option[T])
def gen(x: Int): TC[_] = x match {
case 0 => (classTag[Int], Option[Int](0))
case _ =>...
215 просмотров
schedule
08.04.2022
Разница между экзистенциальными типами Scala и подстановочными знаками Java на примере?
Немного более конкретный, чем вопрос о переполнении стека Что такое экзистенциальный тип? , в чем разница между экзистенциальными типами в Scala и подстановочными знаками в Java, желательно на каком-нибудь иллюстративном примере?
Во всем,...
7108 просмотров
schedule
25.04.2022
Сворачивание полиморфного списка в Haskell
У меня есть коллекция записей разных типов в большом приложении Haskell, которые ссылаются друг на друга. Все задействованные типы реализуют общий класс типов. Класс типов содержит функции, которые работают с переменной и всеми ее дочерними...
1235 просмотров
schedule
28.04.2022
Как определить экзистенциальный тип более высокого типа в Scala
Я пытался определить тип, который принимает экзистенциальный тип более высокого типа в Scala.
К сожалению, Scalac этого не позволяет.
Welcome to Scala version 2.11.7 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_45).
Type in expressions to...
512 просмотров
schedule
25.04.2022
Что делает impl Trait универсальным аргументом и экзистенциальным возвращаемым значением?
Я читал RFC по "расширению " impl Trait , когда я наткнулся на следующее:
Напротив, программист, который сначала изучил: fn take_iter(t: impl
Iterator) , а затем попробовал: fn give_iter() -> impl Iterator , добьется успеха, не имея...
699 просмотров
schedule
29.04.2022
Повторить параметр типа экзистенциального экземпляра
У меня есть такой код:
{-# LANGUAGE AllowAmbiguousTypes #-}
module Foo where
import Data.Proxy
class Foo x y
class Bar x y
class Baz x y
where
baz :: Proxy x -> Proxy y -> ()
instance (Foo a v, Bar b v) => Baz a b
where
baz _ _...
102 просмотров
schedule
19.05.2022
Как я могу выполнить операцию разброса/сбора типов в Haskell?
У меня есть дерево, которое содержит узлы разных типов. Они помечены с использованием типа данных:
data Wrapping = A Int
| B String
Я хочу написать две функции:
scatter :: Wrapping -> a
gather :: a -> Output...
207 просмотров
schedule
11.06.2022
Отображение списка экзистенциальных типов
У меня есть список экзистенциально типизированных объектов, которые я хочу отобразить. Что-то вроде этого:
sealed abstract class IntBox(val v: Int)
case object IB1 extends IntBox(1)
case object IB2 extends IntBox(2)
case class Adder[A <:...
76 просмотров
schedule
18.06.2022
Жонглирование вводом с помощью GADT во время выполнения
Я разрабатываю типизированный формальный язык, то есть формальный язык, в котором каждая буква имеет представление определенного типа. Пока что у меня есть следующее:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}...
113 просмотров
schedule
06.07.2022
Гетерогенная индексированная структура без экзистенциальных типов?
Я пытаюсь создать гетерогенную индексированную структуру и придумал следующее решение, но Мне сказали не использовать экзистенциальные типы .
Вы видите лучшее решение?
Я хотел бы сохранить разделение между определением интерфейсов ( type и...
780 просмотров
schedule
22.07.2022
Определение разрешимого равенства для зависимой пары в Agda
Я пытаюсь определить разрешимое равенство сигма-типа, но застреваю, несмотря на то, что моя цель совпадает с тем, что у меня есть.
module SigmaEqual where
open import Function using (id)
open import Data.Nat using (ℕ) renaming (_≟_ to _≟ℕ_)
open...
376 просмотров
schedule
27.08.2022
