Re: ANNOUNCE: fixpoint 0.1

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: ANNOUNCE: fixpoint 0.1

Bertram Felgenhauer-2
[redirecting from haskell@...]
apfelmus wrote:
[...]
> I wonder whether a multi parameter type class without fundeps/associated
> types would be better.
>
>   class Fixpoint f t where
>     inject  :: f t -> t
>     project ::   t -> f t
>
[...]
> Interestingly, this even gives slightly shorter type signatures
>
>   cata :: Fixpoint f t => (f s -> s) -> t -> s
>   size :: (Fixpoint f t, Foldable f) => t -> Int

size can't be used now though, because there is no way to infer f.

Bertram
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: ANNOUNCE: fixpoint 0.1

Heinrich Apfelmus
Bertram Felgenhauer wrote:

> [redirecting from haskell@...]
> apfelmus wrote:
> [...]
>> I wonder whether a multi parameter type class without fundeps/associated
>> types would be better.
>>
>>   class Fixpoint f t where
>>     inject  :: f t -> t
>>     project ::   t -> f t
>>
> [...]
>> Interestingly, this even gives slightly shorter type signatures
>>
>>   cata :: Fixpoint f t => (f s -> s) -> t -> s
>>   size :: (Fixpoint f t, Foldable f) => t -> Int
>
> size can't be used now though, because there is no way to infer f.

Ah, of course, stupid me.

Making  f  an associacted type synonym / fundep  instead of a associated
data type is still worth it, since we can use it for  Mu f

   class Fixpoint f t where
     type F t a
     ...

   instance Fixpoint f (Mu f) where ..
     type F (Mu f) a = f a

Otherwise, we would have to deal with some kind of newtype

     data F (Mu f) a = MuF f a

Hm, but does  F (Mu f)  qualify as a type constructor of kind  * -> *
for type inference/checking? Or is the situation the same as with normal
type synonyms?


Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: ANNOUNCE: fixpoint 0.1

Roman Leshchinskiy
apfelmus wrote:

> Bertram Felgenhauer wrote:
>> [redirecting from haskell@...]
>> apfelmus wrote:
>> [...]
>>> I wonder whether a multi parameter type class without
>>> fundeps/associated types would be better.
>>>
>>>   class Fixpoint f t where
>>>     inject  :: f t -> t
>>>     project ::   t -> f t
>>>
>> [...]
>>> Interestingly, this even gives slightly shorter type signatures
>>>
>>>   cata :: Fixpoint f t => (f s -> s) -> t -> s
>>>   size :: (Fixpoint f t, Foldable f) => t -> Int
>>
>> size can't be used now though, because there is no way to infer f.
>
> Ah, of course, stupid me.
>
> Making  f  an associacted type synonym / fundep  instead of a associated
> data type is still worth it, since we can use it for  Mu f

I originally considered the following:

class Functor (Pre t) => Fixpoint t where
   type Pre t :: * -> *

instance Fixpoint (Mu f) where
   type Pre (Mu f) = f

But alas, this breaks hylomorphisms:

hylo :: Fixpoint t => (Pre t s -> s) -> (p -> Pre t p) -> p -> s

If Pre is a type function, there is no way to infer t.

Roman

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: ANNOUNCE: fixpoint 0.1

Heinrich Apfelmus
Roman Leshchinskiy wrote:

> apfelmus wrote:
>>
>> Making  f  an associacted type synonym / fundep  instead of a
>> associated data type is still worth it, since we can use it for  Mu f
>
> But alas, this breaks hylomorphisms:
>
> hylo :: Fixpoint t => (Pre t s -> s) -> (p -> Pre t p) -> p -> s
>
> If Pre is a type function, there is no way to infer t.

Ah, right. But unlike  size , this is unambiguous since  t  can (and
probably should) be fused away:

   hylo :: Functor f => (f s -> s) -> (p -> f p) -> p -> s
   hylo f g = f . fmap (hylo f g) . g


Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: ANNOUNCE: fixpoint 0.1

Roman Leshchinskiy
apfelmus wrote:

> Roman Leshchinskiy wrote:
>> apfelmus wrote:
>>>
>>> Making  f  an associacted type synonym / fundep  instead of a
>>> associated data type is still worth it, since we can use it for  Mu f
>>
>> But alas, this breaks hylomorphisms:
>>
>> hylo :: Fixpoint t => (Pre t s -> s) -> (p -> Pre t p) -> p -> s
>>
>> If Pre is a type function, there is no way to infer t.
>
> Ah, right. But unlike  size , this is unambiguous since  t  can (and
> probably should) be fused away:
>
>   hylo :: Functor f => (f s -> s) -> (p -> f p) -> p -> s
>   hylo f g = f . fmap (hylo f g) . g

Excellent point! When I originally developed the code, type functions
didn't really work anyway. I'll try again now that they are more mature.

Roman

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: ANNOUNCE: fixpoint 0.1

Heinrich Apfelmus
Roman Leshchinskiy wrote:

> apfelmus wrote:
>>
>> Ah, right. But unlike  size , this is unambiguous since  t  can (and
>> probably should) be fused away:
>>
>>   hylo :: Functor f => (f s -> s) -> (p -> f p) -> p -> s
>>   hylo f g = f . fmap (hylo f g) . g
>
> Excellent point! When I originally developed the code, type functions
> didn't really work anyway. I'll try again now that they are more mature.

Actually, I don't think that

    hylo :: Fixpoint f t => (f s -> s) -> (p -> f p) -> p -> s
    hylo f g = cata f . ana g

will typecheck, the  t  is still ambiguous. It's just that it's one of
those cases where the type signature is ambiguous but the program isn't.
Well, from a denotational point of view anyway, different  t  will
generate different code for  hylo .


Regards,
apfelmus

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe