| When saying "Big Deal" did you mean
|- highly desirable and somebody should go for it
|- or a terrible amount of work, and who tackles it is probably a
| fool on a hubris trip?
I meant
- a lot of work, including changes to the core System FC language
- we lack enough compelling ca
It sounds like you want this, then:
> gabor :: forall a b.
> (KnownSymbol a, KnownSymbol b)
> => Proxy a -> Proxy b
> -> Either (Equal a b :~: 'False) (a :~: b)
> gabor a b = case sameSymbol a b of
> Just refl -> Right refl
> Nothing -> Left (unsafeCoerce Refl)
>
It st
On 7/27/15, Richard Eisenberg wrote:
> This works for me (with ScopedTypeVariables):
>
>> gabor :: forall a b lhs rhs.
>> (KnownSymbol a, KnownSymbol b)
>> => Proxy a -> Proxy b -> Proxy (lhs :~: rhs)
>> -> Either (lhs :~: rhs) (a :~: b)
>> gabor a b _ = case sameSymbol a b of
This works for me (with ScopedTypeVariables):
> gabor :: forall a b lhs rhs.
> (KnownSymbol a, KnownSymbol b)
> => Proxy a -> Proxy b -> Proxy (lhs :~: rhs)
> -> Either (lhs :~: rhs) (a :~: b)
> gabor a b _ = case sameSymbol a b of
> Just refl -> Right refl
> Nothing ->
On 7/27/15, Richard Eisenberg wrote:
>
> On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:
decideRefl :: Proxy (a :: Symbol) -> Proxy b
-> Proxy (Equal a b :~: 'False)
-> Either (Equal a b :~: 'False) (a :~: b)
>
> What's the point of the third Proxy a
On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:
>>>
>>> decideRefl :: Proxy (a :: Symbol) -> Proxy b
>>> -> Proxy (Equal a b :~: 'False)
>>> -> Either (Equal a b :~: 'False) (a :~: b)
What's the point of the third Proxy argument? I don't think it adds anything.
Perha
On 7/27/15, Richard Eisenberg wrote:
>
> On Jul 27, 2015, at 10:36 AM, Gabor Greif wrote:
>
>> When saying "Big Deal" did you mean
>> - highly desirable and somebody should go for it
>> - or a terrible amount of work, and who tackles it is probably a
>> fool on a hubris trip?
>>
>> (I still hav
On Jul 27, 2015, at 10:36 AM, Gabor Greif wrote:
> When saying "Big Deal" did you mean
> - highly desirable and somebody should go for it
> - or a terrible amount of work, and who tackles it is probably a
> fool on a hubris trip?
>
> (I still have my problems deciphering British irony.)
My u
On Jul 27, 2015, at 9:48 AM, Simon Peyton Jones wrote:
>
> Making type inference (and system FC) exploit negative info would be a Big
> Deal, I think.
Yes. Gabor points out a known infelicity with the interaction between closed
type families and GADTs. But I agree with Simon that fixing it wo
Simon,
yes, this is the the same problem. You probably meant:
=
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy 'False -> Bool
foo x = False
f :: forall a b. Maybe (a :~: b) -> Bool
f x = case x of
Just Refl -> True
Yes. Here's a simpler example:
=
type family Equal a b where
Equal a a = 'True
Equal a b = 'False
foo :: Proxy 'True -> Bool
foo x = True
f :: forall a b. Maybe (a :~: b) -> Bool
f x = case x of
Just Refl -> True
Nothing -> foo (undefined
Hi Anthony,
while I suspected that one would need to go the "value inference"
route (i.e. type classes), I had no idea how to get started. So thanks
for your snippet, it is very helpful.
Otoh, it only strips one segment
``` haskell
*GaborTEq> showPath $ stripOut (Proxy :: Proxy "Hey") (Longer (P
I think you are already very familiar with what I'll show here, but I figured
I'd offer this alternative approach just in case. It does not directly address
your type error, but does show one way of loosely steering values from the type
level.
https://gist.github.com/acowley/57724b6facd6a39a19
13 matches
Mail list logo
