Generalized algebraic data types, GADTs, are a more powerful form of algebraic data types that support custom constructor types.
Questions tagged [gadt]
397 questions
53
votes
2 answers
What does data ... where mean in Haskell?
I saw this snippet at the devlog of omegagb:
data ExecutionAST result where
Return :: result -> ExecutionAST result
Bind :: (ExecutionAST oldres) -> (oldres -> ExecutionAST result) ->
ExecutionAST result
WriteRegister :: M_Register…
wliao
- 1,416
- 11
- 18
51
votes
1 answer
Future of roles for GADT-like type variables?
A question from yesterday had a definition of HList (from the HList package) that uses data families. Basically:
data family HList (l :: [*])
data instance HList '[] = HNil
newtype instance HList (x ': xs) = HCons1 (x, HList xs)
pattern HCons x xs…
Alec
- 31,829
- 7
- 67
- 114
44
votes
5 answers
Real world use of GADT
How do I make use of Generalized Algebraic Data Type?
The example given in the haskell wikibook is too short to give me an insight of the real possibilities of GADT.
Raoul Supercopter
- 5,076
- 1
- 34
- 37
30
votes
2 answers
Why GADT/existential data constructors cannot be used in lazy patterns?
Today, I got a compiler error when trying to use a lazy pattern when matching on an existential GADT constructor:
An existential or GADT data constructor cannot be used inside a lazy (~) pattern
Why is that limitation? What "bad" stuff could…
Petr
- 62,528
- 13
- 153
- 317
21
votes
1 answer
Odd ghc error message, "My brain just exploded"?
When I try to pattern-match a GADT in an proc syntax (with Netwire and Vinyl):
sceneRoot = proc inputs -> do
let (Identity camera :& Identity children) = inputs
returnA -< (<*>) (map (rGet draw) children) . pure
I get the…
Dan
- 12,409
- 3
- 50
- 87
20
votes
1 answer
When are refutation cases necessary in OCaml?
In the GADTs section of the "Language extensions" chapter of the official OCaml docs, refutation cases of the form _ -> . are introduced. However, I thought that pattern-matching was already exhaustive, so I'm not sure when a refutation case is…
Kevin Ji
- 10,479
- 4
- 40
- 63
20
votes
2 answers
How can I recover sharing in a GADT?
In Type-Safe Observable Sharing in Haskell Andy Gill shows how to recover sharing that existed on the Haskell level, in a DSL. His solution is implemented in the data-reify package. Can this approach be modified to work with GADTs? For example,…
tibbe
- 8,809
- 7
- 36
- 64
17
votes
1 answer
How do you allow GADTs in Haskell?
Today I started to learn about GADTs from: haskell.org and https://wiki.haskell.org
Unfortunately, I don't know how to use them. If I run the code from the example I get the following error:
[1 of 1] Compiling Main ( test.hs, interpreted…
maffh
- 299
- 3
- 12
16
votes
1 answer
Equality for GADTs which erase type parameter
I cannot implement an instance of Eq for the following typesafe DSL for expressions implemented with GADTs.
data Expr a where
Num :: Int -> Expr Int
Bool :: Bool -> Expr Bool
Plus :: Expr Int -> Expr Int -> Expr Int
If :: Expr Bool -> Expr a…
kajigor
- 308
- 1
- 6
16
votes
2 answers
Defining Eq instance for Haskell GADTs
I have a GADT that's a lot like this:
data In a where
M :: MVar a -> In a
T :: TVar a -> In a
F :: (a -> b) -> In a -> In b
It wraps various input primitives, but the last constructor also allows for a Functor instance:
instance Functor In…
Neil Brown
- 3,558
- 1
- 27
- 36
16
votes
2 answers
Fundeps and GADTs: When is type checking decidable?
I was reading a research paper about Haskell and how HList is implemented and wondering when the techniques described are and are not decidable for the type checker. Also, because you can do similar things with GADTs, I was wondering if GADT type…
Jason Dagit
- 13,684
- 8
- 33
- 56
16
votes
3 answers
How to put constraints on type variable of kind `Constraint`?
I'm playing around with the ConstraintKinds extension of GHC.
I have the following data type, which is just a box for things fulfilling some one parameter constraint c:
data Some (c :: * -> Constraint) where
Some :: forall a. c a => a -> Some…
Tobias Brandt
- 3,393
- 18
- 28
16
votes
5 answers
Understanding the limits of Scala GADT support
The error in Test.test seems unjustified:
sealed trait A[-K, +V]
case class B[+V]() extends A[Option[Unit], V]
case class Test[U]() {
def test[V](t: A[Option[U], V]) = t match {
case B() => null // constructor cannot be instantiated to…
Patrick Prémont
- 948
- 7
- 13
15
votes
1 answer
Parametrized Inductive Types in Agda
I'm just reading Dependent Types at Work. In the introduction to parametrised types, the author mentions that in this declaration
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
the type of List is Set → Set and that A…
Vitus
- 11,822
- 7
- 37
- 64
15
votes
1 answer
Pattern matching in Observational Type Theory
In the end of the "5. Full OTT" section of Towards Observational Type Theory the authors show how to define coercible-under-constructors indexed data types in OTT. The idea is basically to turn indexed data types into parameterized like this:
data…
effectfully
- 12,325
- 2
- 17
- 40