Re: [Haskell-cafe] Pattern matching with singletons
Very helpful, thanks! I may come back with more singleton/type families
questions :)
On Tue, Mar 26, 2013 at 6:41 PM, Richard Eisenberg e...@cis.upenn.eduwrote:
Hello Paul,
- Forwarded message from Paul Brauner polux2...@gmail.com -
snip
- is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
SLeft, ... (in which case GHC could infer it but for some reason can't)
- or are these pattern + definitions not sufficient to prove that a
~ ('CC ('Left 'CA)) no matter what?
The first one. GHC can deduce that (a ~ ('CC ('Left b))), for some fresh
variable (b :: TA), but it can't yet take the next step and decide that,
because TA has only one constructor, b must in fact be 'CA. In type-theory
lingo, this deduction is called eta-expansion. There have been on-and-off
debates about how best to add this sort of eta-expansion into GHC, but all
seem to agree that it's not totally straightforward. For example, see GHC
bug #7259. There's a non-negligible chance I will be taking a closer look
into this at some point, but not for a few months, so don't hold your
breath. I'm not aware of anyone else currently focusing on this problem
either, I'm afraid.
I'm glad you're finding use in the singletons package! Let me know if I
can be of further help.
Richard
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Pattern matching with singletons
Hello Paul,
- Forwarded message from Paul Brauner polux2...@gmail.com -
snip
- is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
SLeft, ... (in which case GHC could infer it but for some reason can't)
- or are these pattern + definitions not sufficient to prove that a
~ ('CC ('Left 'CA)) no matter what?
The first one. GHC can deduce that (a ~ ('CC ('Left b))), for some fresh
variable (b :: TA), but it can't yet take the next step and decide that,
because TA has only one constructor, b must in fact be 'CA. In type-theory
lingo, this deduction is called eta-expansion. There have been on-and-off
debates about how best to add this sort of eta-expansion into GHC, but all seem
to agree that it's not totally straightforward. For example, see GHC bug #7259.
There's a non-negligible chance I will be taking a closer look into this at
some point, but not for a few months, so don't hold your breath. I'm not aware
of anyone else currently focusing on this problem either, I'm afraid.
I'm glad you're finding use in the singletons package! Let me know if I can be
of further help.
Richard
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Pattern matching with singletons
Hello,
the following programs seems to hit either some limitation of GHC or maybe
I'm just missing something and it behaves the intended way.
{-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds, GADTs #-}
module Test where
import Data.Singletons
data TA = CA
data TB = CB
data TC = CC (Either TA TB)
$(genSingletons [''TA, ''TB, ''TC])
type family Output (x :: TC) :: *
type instance Output ('CC ('Left 'CA)) = Int
type instance Output ('CC ('Right 'CB)) = String
f :: Sing (a :: TC) - Output a
f (SCC (SLeft SCA)) = 1
g :: Sing (a :: TC) - Output a
g (SCC (SLeft _)) = 1
Function f typechecks as expected. Function g fails to typecheck with the
following error.
Could not deduce (Num (Output ('CC ('Left TA TB n0
arising from the literal `1'
from the context (a ~ 'CC n, SingRep (Either TA TB) n)
bound by a pattern with constructor
SCC :: forall (a_a37R :: TC) (n_a37S :: Either TA TB).
(a_a37R ~ 'CC n_a37S, SingRep (Either TA TB)
n_a37S) =
Sing (Either TA TB) n_a37S - Sing TC a_a37R,
in an equation for `g'
at Test.hs:21:4-16
or from (n ~ 'Left TA TB n0,
SingRep TA n0,
SingKind TA ('KindParam TA))
bound by a pattern with constructor
SLeft :: forall (a0 :: BOX)
(b0 :: BOX)
(a1 :: Either a0 b0)
(n0 :: a0).
(a1 ~ 'Left a0 b0 n0, SingRep a0 n0,
SingKind a0 ('KindParam a0)) =
Sing a0 n0 - Sing (Either a0 b0) a1,
in an equation for `g'
at Test.hs:21:9-15
Possible fix:
add an instance declaration for
(Num (Output ('CC ('Left TA TB n0
In the expression: 1
In an equation for `g': g (SCC (SLeft _)) = 1
I would expect that a ~ ('CC ('Left 'CA)) in the right hand-side of g (SCC
(SLeft _)) = 1 since SLeft's argument is necessarily of type STA, whose
sole inhabitant is SA.
Now I understand (looking at -ddump-slices, the singletons' library paper
and the error message) that the definition of SCC and SLeft
don't immediately imply what I just wrote above. So my question is: in the
right hand-side of g (SCC (SLeft _)) = 1,
- is a ~ ('CC ('Left 'CA)) a consequence of the definitions of SCC,
SLeft, ... (in which case GHC could infer it but for some reason can't)
- or are these pattern + definitions not sufficient to prove that a
~ ('CC ('Left 'CA)) no matter what?
Cheers,
Paul
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
