gadt Questions
1
Solved
Data.Dynamic has the following implementation:
data Dynamic where
Dynamic :: TypeRep a -> a -> Dynamic
It has occurred to me that the following definition would be equivalent (at least I th...
1
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 ...
1
Using:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveDataTypeable #-}
And given the following datatype:
data Event a where
PureE :: a -> Event a
MapE ...
2
Solved
https://youtu.be/brE_dyedGm0?t=1362
data T a where
T1 :: Bool -> T Bool
T2 :: T a
f x y = case x of
T1 x -> True
T2 -> y
Simon is saying that f could be typed as T a -> a -> ...
1
Solved
Phantom type makes pattern matching irrefutable, but that seemingly does not work inside do notation
Please look at the code. I believe using phantom type makes the pattern matching irrefutable so there is no need in MonadFail instance.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# OPTION...
1
In the following code:
class FD a b | a -> b
data Foo a where
Foo :: FD a b => b -> Foo a
unFoo :: FD a b => Foo a -> b
unFoo (Foo x) = x
By common sense this should work, since ...
Hallowmas asked 25/11, 2021 at 13:54
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
1
Solved
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 ...
1
Solved
Is the extension GADT in Haskell destroying polymorphism, even in code that don't use GADTs ?
Here's a example which works and don't use GADT
{-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE GADTs #-}
...
Appear asked 21/3, 2021 at 14:37
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
Consider this code:
{-# LANGUAGE GADTs #-}
data P t where
PA :: P Int
PB :: P Double
PC :: P Char
isA PA = True
isA _ = False
It compiles and works fine. Now consider this code:
{-# LANGUA...
Tendon asked 2/4, 2020 at 14:43
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
Continuing my crusade against MonadFail being a constraint in my monad, I'm now faced with the following:
data Thing :: Bool -> Type where
TrueThing :: Thing 'True
FalseThing :: Thing 'False
...
1
Solved
I have wrapped up whole data family in a single existential:
data Type = Numeric | Boolean
data family Operator (t :: Type)
data instance Operator 'Numeric = Add | Sub
data instance Operator 'Bo...
Reitman asked 28/10, 2019 at 11:32
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
3
Solved
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 :: * -> Co...
3
Following on from this q about GADTs, I'm trying to build an EDSL (for the example in the paper) but without GADTs. I have got something working that avoids doubling-up the datatypes for the AST; b...
Ermey asked 7/3, 2019 at 5:38
1
Solved
The typical examples for the benefits of a GADT are representing the syntax for a DSL; say here on the wiki or the PLDI 2005 paper.
I can see that if you have a AST that's type-correct by construc...
3
Solved
Consider the following code:
data (:+:) f g a = Inl (f a) | Inr (g a)
data A
data B
data Foo l where
Foo :: Foo A
data Bar l where
Bar :: Bar B
type Sig = Foo :+: Bar
fun :: Sig B -> Int...
1
Solved
I am trying to make use of GADTs to have well constrained types, but some dependencies are impossible to handle during compilation time – for example user input. Let's consider following AVL tree d...
3
Solved
I made a variant of eqT that would allow me work with the result like any other Bool to write something like eqT' @a @T1 || eqT' @a @T2. However, while that worked well in some cases, I found that ...
1
Solved
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 a...
Ada asked 13/10, 2018 at 16:52
2
What/why are the differences between those three? Is a GADT (and regular data types) just a shorthand for a data family? Specifically what's the difference between:
data GADT a where
MkGADT :: In...
1
Solved
For educational purposes, I have been trying to reconstruct an example from the book "Type-Driven Development with Idris" (namely RemoveElem.idr) in Haskell via use of various language extensions a...
Glycogen asked 19/8, 2018 at 10:36
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 Next >
© 2022 - 2024 — McMap. All rights reserved.