existential-type Questions

1

I have an existential type defined like this: trait Collection { type Element; } impl<T> Collection for Vec<T> { type Element = T; } type Existential<T> = impl Collection<E...
Calque asked 24/4, 2019 at 9:25

1

Solved

I found that this piece of code generates no errors protocol Foo{ func foo() } let x: Foo? = nil While the following starts complaining Use of protocol 'Foo' as a type must be written 'any Foo' ...
Palaeography asked 23/5, 2023 at 6:23

3

Solved

I'm trying to use a GADT with DataKinds, as shown below {-# LANGUAGE KindSignatures, DataKinds, GADTs #-} module NewGadt where data ExprType = Var | Nest data Expr (a :: ExprType) where ExprVar ...
Cower asked 10/9, 2021 at 21:42

2

This thread addressed how to use TypeTag to get runtime type of type parameters when used with Existential type. Another thread addressed how to cast a variable to its runtime type retrieved from T...
Homocyclic asked 1/4, 2015 at 20:43

1

Solved

Starting Scala 3 existential types have been dropped and one of the reasons is stated as Existential types largely overlap with path-dependent types, so the gain of having them is relatively minor...
Swirsky asked 18/4, 2021 at 13:4

3

Solved

I was trying to grasp the concept of existential types in Haskell using the article Haskell/Existentially quantified types. At the first glance, the concept seems clear and somewhat similar to gene...
Comatose asked 18/2, 2021 at 6:33

1

Solved

Consider the following simple example involving Aux-pattern: sealed trait AdtBase abstract case class Foo(){ type T <: AdtBase } object Foo{ type Aux[TT] = Foo { type T = TT } } abstract ca...
Beanpole asked 4/11, 2020 at 1:5

1

Solved

I'm trying to copy() a Scala case class which has a type param. At the call site, the type of the value is Foo[_]. This compiles as expected: case class Foo[A](id: String, name: String, v1: Bar[A])...

1

I've got some code like this: {-# 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 -> () inst...
Almshouse asked 6/7, 2020 at 0:29

1

Solved

Still playing with existentials over constraints (just exploring this design space, I know it is considered bad by many Haskellers). See this question for more info. {-# LANGUAGE RankNTypes #-} {-#...
Virology asked 1/7, 2020 at 8:50

4

Solved

I have a custom value type Value labeled by its type ValType: data ValType = Text | Bool data Value (tag :: ValType) where T :: Text -> Value 'Text B :: Bool -> Value 'Bool and I would ...
Riella asked 20/6, 2020 at 13:48

2

Solved

I am trying to understand Existential types in Haskell and came across a PDF http://www.ii.uni.wroc.pl/~dabi/courses/ZPF15/rlasocha/prezentacja.pdf Please correct my below understandings that I ha...
Desultory asked 5/2, 2020 at 17:1

1

Consider this Vect type: {-# LANGUAGE GADTs, DataKinds, KindSignatures, RankNTypes #-} import Data.Kind (Type) data Nat = Zero | Succ Nat data Vect :: Nat -> Type -> Type where Nil :: Ve...

2

Solved

What exactly is the difference between these? I think I understand how existential types work, they are like having a base class in OO without a way to down cast. How are universal types different?...
Accelerant asked 13/1, 2013 at 1:7

2

Solved

I have the following toy implementation of a non-empty list (NEList) datatype: -- A type to describe whether or not a list is empty. data Emptiness :: Type where Empty :: Emptiness NotEmpty :: E...
Comparative asked 12/9, 2019 at 23:28

2

Solved

Lately I have been playing with this type, which I understand to be an encoding of the free distributive functor (for tangential background on that, see this answer): data Ev g a where Ev :: ((g ...
Azotemia asked 30/6, 2019 at 17:27

4

Solved

I'm currently facing a problem in C# that I think could be solved using existential types. However, I don't really know if they can be created in C#, or simulated (using some other construct). Bas...
Liddell asked 9/9, 2015 at 18:12

11

Solved

I read through the Wikipedia article Existential types. I gathered that they're called existential types because of the existential operator (∃). I'm not sure what the point of it is, though. What'...
Tepid asked 15/11, 2008 at 7:31

0

In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respe...
Byron asked 19/11, 2018 at 13:33

1

data T t where A :: Show (t a) => t a -> T t B :: Coercible Int (t a) => t a -> T t f :: T t -> String f (A t) = show t g :: T t -> Int g (B t) = coerce t Why does f compile...
Newsome asked 23/7, 2018 at 2:15

1

Are there any examples anywhere of how to use the DMap type? The package documentation is very learned, and I know it if for reference only, but it is singularly unhelpful for one getting started. ...
Hardfavored asked 18/5, 2017 at 6:23

2

Solved

I'd love to get the following example to type-check: {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module Foo wh...
Phallicism asked 3/5, 2018 at 15:59

1

Solved

When would one want to use a specialized existential type vs. a dependent pair (also called a dependent sum or sigma type)? Here is an example. The following is a length-indexed list and dependen...

2

Solved

Does the following bit of code use dynamic dispatch as it's understood in C++ or Java? As I understand, at the last line, compiler cannot possibly know at compile time which implementation of (==)...
Handyman asked 22/4, 2018 at 6:18

1

Solved

Suppose that we have defined an existential type: type T = (X => X, X) forSome { type X } and then defined a list of type List[T]: val list = List[T]( ((x: Int) => x * x, 42), ((_: Stri...

© 2022 - 2024 — McMap. All rights reserved.