Dear all, I wanted to voice support for a partial type annotations. Here's my usage scenario: I have a monad for an imperative EDSL, which has an associated expression data type, class (Monad m, Expression (ExprTyp m)) => MyDSLMonad m where data ExprTyp m :: * -> * and you write imperative EDSL code like so, my_code_block = do x <- instruction1 y <- instruction2 (x + x) ... I want the user to be able to annotate "x is an Integer". However, to do that now, one has to now add a type signature for my_code_block like so, so that the $m$ variable is in scope, my_code_block :: forall m. MyDSLMonad m => m () my_code_block = do x :: ExprTyp m Integer <- instruction1 ... If such a feature were available, one could write a nice type synonym "Expr" and use it like so, type Expr a = ExprTyp _ a my_code_block = do x :: Expr Integer <- instruction1 Suggestions for workarounds are appreciated. I created an `asExprTypeOf`, similar to Prelude's `asExprTyp`, but I don't like the syntax as much. Some previous discussion * http://www.haskell.org/pipermail/haskell/2002-April/009409.html * (a reply) http://www.haskell.org/pipermail/haskell/2002-April/009413.html * http://hackage.haskell.org/trac/haskell-prime/wiki/PartialTypeAnnotations cheers, Nicholas — https://ntung.com — 4432-nstung
On 20.01.2012 00:37, Nicholas Tung wrote:
Dear all,
I wanted to voice support for a partial type annotations. Here's my usage scenario: I have a monad for an imperative EDSL, which has an associated expression data type,
I wanted such extension more than once. For me it's useful when compiler can almost infer type and only few type variables are actually required. Now I have to either type full signature or invert functions a la `asTypeOf'
class (Monad m, Expression (ExprTyp m)) => MyDSLMonad m where data ExprTyp m :: * -> *
and you write imperative EDSL code like so,
my_code_block = do x <- instruction1 y <- instruction2 (x + x) ...
I want the user to be able to annotate "x is an Integer". However, to do that now, one has to now add a type signature for my_code_block like so, so that the $m$ variable is in scope,
my_code_block :: forall m. MyDSLMonad m => m () my_code_block = do x :: ExprTyp m Integer <- instruction1
Actually it should be
my_code_block :: ... my_code_block = do x :: Integer <- instruction1 -- Require ScopedTypeVariables
or
x <- instruction1 :: Expr Integer
or with partial type signatures
x <- instruction1 :: _ _ Integer
or wiht
x <- instruction1 y <- instrunctio2 (x + x :: Integer)
On Thu, Jan 19, 2012 at 13:16, Aleksey Khudyakov
On 20.01.2012 00:37, Nicholas Tung wrote:
Dear all,
I wanted to voice support for a partial type annotations. Here's my usage scenario: I have a monad for an imperative EDSL, which has an associated expression data type,
I wanted such extension more than once. For me it's useful when compiler can almost infer type and only few type variables are actually required. Now I have to either type full signature or invert functions a la `asTypeOf'
class (Monad m, Expression (ExprTyp m)) => MyDSLMonad m where
data ExprTyp m :: * -> *
and you write imperative EDSL code like so,
my_code_block = do x <- instruction1 y <- instruction2 (x + x) ...
I want the user to be able to annotate "x is an Integer". However, to do that now, one has to now add a type signature for my_code_block like so, so that the $m$ variable is in scope,
my_code_block :: forall m. MyDSLMonad m => m () my_code_block = do x :: ExprTyp m Integer <- instruction1
Actually it should be
my_code_block :: ... my_code_block = do x :: Integer <- instruction1 -- Require ScopedTypeVariables
or
x <- instruction1 :: Expr Integer
or with partial type signatures
x <- instruction1 :: _ _ Integer
or wiht
x <- instruction1 y <- instrunctio2 (x + x :: Integer)
It's not important, but my example was what I meant -- I am creating an EDSL, and the values flowing through are actually syntax trees representing expressions. For example, "x + x" might create a tree with top node "+", and subtrees as "x". We then have type instruction1 :: m (ExprTyp m Integer) or using the shorthand, if there were partial signatures, instruction1 :: m (Expr Integer) regards, Nicholas — https://ntung.com — 4432-nstung
Hi,
x :: Integer <- instruction1 -- Require ScopedTypeVariables
Indeed, that does require ScopedTypeVariables to be enabled, but this basic use case is not clearly covered in the ScopedTypeVariables documentation. Also, it is not clear to me why ScopedTypeVariables is required at all here, as Integer is a literal type and not a signature-bound type variable. -- Paul
Hi, On 20.01.2012, at 09:30, Paul R wrote:
Hi,
x :: Integer <- instruction1 -- Require ScopedTypeVariables
This is still enabled by the PatternSignatures extensions.
Indeed, that does require ScopedTypeVariables to be enabled, but this basic use case is not clearly covered in the ScopedTypeVariables documentation.
http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extension...
Also, it is not clear to me why ScopedTypeVariables is required at all here, as Integer is a literal type and not a signature-bound type variable.
In current GHC version PatternSignatures is deprecated and instead integrated into ScopedTypeVariables. Jean
Oleg has described a grody hack which achieves this effect. http://okmij.org/ftp/Haskell/types.html#partial-sigs I agree more first class support for this would be nice. Edward Excerpts from Nicholas Tung's message of Thu Jan 19 15:37:28 -0500 2012:
Dear all,
I wanted to voice support for a partial type annotations. Here's my usage scenario: I have a monad for an imperative EDSL, which has an associated expression data type,
class (Monad m, Expression (ExprTyp m)) => MyDSLMonad m where data ExprTyp m :: * -> *
and you write imperative EDSL code like so,
my_code_block = do x <- instruction1 y <- instruction2 (x + x) ...
I want the user to be able to annotate "x is an Integer". However, to do that now, one has to now add a type signature for my_code_block like so, so that the $m$ variable is in scope,
my_code_block :: forall m. MyDSLMonad m => m () my_code_block = do x :: ExprTyp m Integer <- instruction1 ...
If such a feature were available, one could write a nice type synonym "Expr" and use it like so,
type Expr a = ExprTyp _ a
my_code_block = do x :: Expr Integer <- instruction1
Suggestions for workarounds are appreciated. I created an `asExprTypeOf`, similar to Prelude's `asExprTyp`, but I don't like the syntax as much.
Some previous discussion * http://www.haskell.org/pipermail/haskell/2002-April/009409.html * (a reply) http://www.haskell.org/pipermail/haskell/2002-April/009413.html * http://hackage.haskell.org/trac/haskell-prime/wiki/PartialTypeAnnotations
cheers, Nicholas — https://ntung.com — 4432-nstung
On Thu, Jan 19, 2012 at 15:02, Edward Z. Yang
Oleg has described a grody hack which achieves this effect.
http://okmij.org/ftp/Haskell/types.html#partial-sigs
I agree more first class support for this would be nice.
Edward
That's an amusing hack, but does it provide anything on top of `asTypeOf`? I'd rather write Oleg's first example as, isOrd :: Ord a => a isOrd = undefined asOrd = flip asTypeOf isOrd f x = Just $ asOrd x -- now has type Ord a => a -> Maybe a Actually, using view patterns, one can get closer to the code I wanted to write, f (asOrd -> x) = Just x comp x = do (asOrd -> y) <- return x return y But, ideally, I want type expressions to appear as types, not value functions.
In the spirit of Oleg's hack, but with nicer combinator support, you can use the patch combinators I just uploaded to Hackage (prompted by this thread): http://hackage.haskell.org/package/patch-combinators Your example then becomes: my_code_block = do x <- instruction1 -:: tCon (tCon tInteger) y <- instruction2 (x + x) The signature `tCon (tCon tInteger)` should be read as the type `_ (_ Integer)`. Alternatively, with ViewPatterns, you can write: my_code_block2 = do (tCon tInteger -> x) <- instruction1 y <- instruction2 (x + x) return y / Emil 2012-01-19 21:37, Nicholas Tung skrev:
Dear all,
I wanted to voice support for a partial type annotations. Here's my usage scenario: I have a monad for an imperative EDSL, which has an associated expression data type,
class (Monad m, Expression (ExprTyp m)) => MyDSLMonad m where data ExprTyp m :: * -> *
and you write imperative EDSL code like so,
my_code_block = do x <- instruction1 y <- instruction2 (x + x) ...
I want the user to be able to annotate "x is an Integer". However, to do that now, one has to now add a type signature for my_code_block like so, so that the $m$ variable is in scope,
my_code_block :: forall m. MyDSLMonad m => m () my_code_block = do x :: ExprTyp m Integer <- instruction1 ...
If such a feature were available, one could write a nice type synonym "Expr" and use it like so,
type Expr a = ExprTyp _ a
my_code_block = do x :: Expr Integer <- instruction1
Suggestions for workarounds are appreciated. I created an `asExprTypeOf`, similar to Prelude's `asExprTyp`, but I don't like the syntax as much.
Some previous discussion * http://www.haskell.org/pipermail/haskell/2002-April/009409.html * (a reply) http://www.haskell.org/pipermail/haskell/2002-April/009413.html * http://hackage.haskell.org/trac/haskell-prime/wiki/PartialTypeAnnotations
cheers, Nicholas — https://ntung.com — 4432-nstung
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (6)
-
Aleksey Khudyakov -
Edward Z. Yang -
Emil Axelsson -
Jean-Marie Gaillourdet -
Nicholas Tung -
Paul R