Advise on small issues while porting Haskells Pipes package to Idris

[Patrick Wheeler]

In an attempt to learn idris I have ported some of Haskell's Pipes package to idris:

https://github.com/Davorak/Haskell-Pipes-Library/tree/idris

Pipes hackage page:

http://hackage.haskell.org/package/pipes

Pipes.Lift, operators that depend on pipes lift and a few other functions have not yet been ported.

I have a few issues that I am working through and was hoping to receive some advise on how to improve the work so far. Or for example weather issue (2) is a compiler error or an error in my understand of what should compile.

1) One issue that I have run into is that when a worker wrapper transformations is used type inference fails and it not obvious to me how to properly annotate the local working function.

In the below example the Functor instance works correctly when the worker wrapper is unwrapped.  Commented out is the code that is not compiling and the error reported by the repl.

data Proxy  : Type -> Type -> Type -> Type -> (Type -> Type) -> Type -> Type where

    Request : a' -> (a  -> Proxy a' a b' b m r ) -> Proxy a' a b' b m r

    Respond : b  -> (b' -> Proxy a' a b' b m r ) -> Proxy a' a b' b m r

    M       : m (Proxy a' a b' b m r) -> Proxy a' a b' b m r

    Pure    : r -> Proxy a' a b' b m r

instance (Monad m) => Functor (Proxy a' a b' b m) where

     map f p = case p of

                        Request a' fa  => Request a' (\a  => map f (fa  a ))

                        Respond b  fb' => Respond b  (\b' => map f (fb' b'))

                        M          m   => M (m >>= \p' => return (map f p'))

                        Pure    r      => Pure (f r)

{- The follow erro is caused by using the Functor instance below.

ExampleProblems.idr:24:53:

When elaborating right hand side of ExampleProblems.case block in Prelude.Functor.Proxy a' a b' b m instance of Prelude.Functor.Functor, method map, go:

When elaborating argument p1 to Prelude.Functor.Proxy a' a b' b m instance of Prelude.Functor.Functor, method map, go:

        Can't unify

                Proxy a'1 a b' b m a1

        with

                Proxy a' a b' b m a1

        Specifically:

                Can't unify

                        a'1

                with

                        a'

          

instance Monad m => Functor (Proxy a' a b' b m) where

    map f p0 = go p0 where 

        go p = case p of

            Request a' fa  => Request a' (\a  => go (fa  a ))

            Respond b  fb' => Respond b  (\b' => go (fb' b'))

            M          m   => M (m >>= \p' => return (go p'))

            Pure    r      => Pure (f r)

-} 

2) A second problem is that some functionality seems to be working in the repl but not when I try to compile it.

> runEffect $ for (each [1..1]) (lift . print) -- does not report type error

io_bind (io_bind (io_bind (MkIO (\{w0} =>

                                   mkForeignPrim (FFun "putStr" [FString] FUnit)

                                                 (prim__concat (show 1) "\n")

                                                 w))

                          (\{r0} => io_return (Pure r)))

                 (\p' =>

                    io_return (case block in bbind IO

                                                   X

                                                   ()

                                                   ()

                                                   X

                                                   ()

                                                   ()

                                                   (constructor of Prelude.Monad.Monad (\{meth0} =>

                                                                                          \{meth1} =>

                                                                                            \{meth2} =>

                                                                                              \{meth3} =>

                                                                                                io_bind meth

                                                                                                        meth))

                                                   p'

                                                   (\{b'0} => Pure ())

                                                   p')))

        (Pipes.Core.runEffect, go IO

                                  ()

                                  (constructor of Prelude.Monad.Monad (\{meth0} =>

                                                                         \{meth1} =>

                                                                           \{meth2} =>

                                                                             \{meth3} =>

                                                                               io_bind meth

                                                                                       meth))) : IO ()

But when compiled with `idris Main.idr -o Main` does no produce an executable.

file:

module Main

import Pipes.Prelude

main : IO ()

main = runEffect $ for (each [1..3]) (lift . print)

Command line:

$ ~/.cabal/bin/idris Main.idr -o Main

./Pipes/Internal.idr:77:6:Prelude.Functor.Proxy a' a b' b m instance of Prelude.Functor.Functor, method map is possibly not total due to: Prelude.Functor.case block in Proxy a' a b' b m instance of Prelude.Functor.Functor, method map

./Pipes/Internal.idr:103:5:Prelude.Applicative.Proxy a' a b' b m instance of Prelude.Applicative.Applicative, method <$> is possibly not total due to: Prelude.Applicative.case block in Proxy a' a b' b m instance of Prelude.Applicative.Applicative, method <$>

./Pipes/Internal.idr:119:5:Prelude.Monad.Proxy a' a b' b m instance of Prelude.Monad.Monad, method >>= is possibly not total due to: Pipes.Internal.bbind

./Pipes/Internal.idr:185:5:Control.Monad.Reader.r, Proxy a' a b' b m instance of Control.Monad.Reader.MonadReader, method local is possibly not total due to: Control.Monad.Reader.case block in r, Proxy a' a b' b m instance of Control.Monad.Reader.MonadReader, method local

./Pipes/Internal.idr:77:6:Cannot compile:

  Prelude.Functor.Proxy a' a b' b m instance of Prelude.Functor.Functor, method map is possibly not total due to: Prelude.Functor.case block in Proxy a' a b' b m instance of Prelude.Functor.Functor, method map

`./Pipes/Internal.idr:77:6:Cannot compile:` <- This is where the Functor is defined for Proxy

3) Running code like:

    runEffect $ stdinLn >-> take 3 >-> stdoutLn

In the repl seems to be non-terminating. In particular anything that uses fromHandler:

https://github.com/Davorak/Haskell-Pipes-Library/blob/89ca57de8ea6d833e44fb65c512b51e52d84cbcf/src/Pipes/Prelude.idr#L193

4) The forth issue I am having is recreating Haskell type synonym functionality. What I am using right now:

https://github.com/Davorak/Haskell-Pipes-Library/blob/89ca57de8ea6d833e44fb65c512b51e52d84cbcf/src/Pipes/Core.idr#L181

Producer' : {x' : Type} -> {x : Type} -> Type -> (Type -> Type) -> Type -> Type
Producer' {x'} {x} a = Proxy x' x () a

But the when I use it in a function like `yield`:

yield : Monad m => a -> Producer' {x'} {x} a m ()
yield = respond

I end up having to supply all 6 type parameters anyway, which is normally avoid in Haskell with type synonym. So it seems like I might as well use `Proxy` directly.

It does allow for yield to be used as  a `Producer` or a `Pipe` which is the intended purpose of the `Producer'` type synonym.

-- 

Patrick Wheeler

[Jonathan Coveney]

Including gabriel Gonzalez on this email, the creator of pipes. I asked him and he said he'd be interested in helping, as he is also quite interested in Idris. He mentioned an attempt in Agda and can perhaps share some of the pitfalls.

--
You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Patrick Wheeler]

This, [1], SO question, commented on by Edwin Brady, probably answers my question (4) for now. It looks like the functionality to easily match Haskell's type synonyms does not yet exist for Idris.

[1] http://stackoverflow.com/q/22880309

--

Patrick Wheeler
Patrick.Jo...@gmail.com
Patrick...@colorado.edu

[Melvar Chen]

This might have something to do with the missing type signature for go, and/or with you naming different things the same everywhere (in particular variables the same as their types, even when both are in scope at the same time! They’re not separate namespaces here, remember?).
 

This is probably because the instance above failed to typecheck, so idris doesn’t have a working implementation for it. The evaluator will happily reduce a partially defined expression as far as it can, otherwise it wouldn’t be much good for typechecking.

3) Running code like:

    runEffect $ stdinLn >-> take 3 >-> stdoutLn

In the repl seems to be non-terminating. In particular anything that uses fromHandler:

https://github.com/Davorak/Haskell-Pipes-Library/blob/89ca5

3) Running code like:

    runEffect $ stdinLn >-> take 3 >-> stdoutLn

In the repl seems to be non-terminating. In particular anything that uses fromHandler:

https://github.com/Davorak/Haskell-Pipes-Library/blob/89ca57de8ea6d833e44fb65c512b51e52d84cbcf/src/Pipes/Prelude.idr#L193

That looks like it infinitely expands, so I’m not sure what you’re expecting there.

4) The forth issue I am having is recreating Haskell type synonym functionality. What I am using right now:

https://github.com/Davorak/Haskell-Pipes-Library/blob/89ca57de8ea6d833e44fb65c512b51e52d84cbcf/src/Pipes/Core.idr#L181

Producer' : {x' : Type} -> {x : Type} -> Type -> (Type -> Type) -> Type -> Type

Producer' {x'} {x} a = Proxy x' x () a

But the when I use it in a function like `yield`:

yield : Monad m => a -> Producer' {x'} {x} a m ()
yield = respond

I end up having to supply all 6 type parameters anyway, which is normally avoid in Haskell with type synonym. So it seems like I might as well use `Proxy` directly.

It does allow for yield to be used as  a `Producer` or a `Pipe` which is the intended purpose of the `Producer'` type synonym.

The translation of the corresponding Haskell is:
  Producer' : Type -> (Type -> Type) -> Type -> Type
  Producer' b m r = (x', x : Type) -> Proxy x' x () b m r
 
Universal quantification = dependent function type. Of course, I don’t believe that is what you want, since it means you get to mention the two arguments everywhere, but you can’t have implicit arguments outside of the top level, so this is all there is.

-- 

Patrick Wheeler

[Patrick Wheeler]

> This might have something to do with the missing type signature for go, and/or with you naming different things the same everywhere (in particular variables the same as their types, even when both are in scope at the same time! They’re not separate namespaces here, remember?).

I figured that go needed some a type signature/hint, however I was not able to find one that works as of yet. Most of the time when using a worker wrapper like go idris does not need the type hint and I am unsure what is causing the problem in this case.  My best guess was that it might be due to the potential lack of totality.

Thanks, for suggesting using different parameter names in the type signature and in the function.  Unfortunately this did not get go to be excepted.

I have been trying to find a method of referencing types in `map`s type signature in local to this instance. However the repl seems to be rejecting my efforts to add a type signature in in the instance.

> This is probably because the instance above failed to typecheck, so idris doesn’t have a working implementation for it. The evaluator will happily reduce a partially defined expression as far as it can, otherwise it wouldn’t be much good for typechecking.

I cannot identify the failed type checking in the compiler output.

Did you mean ``./Pipes/Internal.idr:77:6:Cannot compile:` the statement about the potential lack of totality?  Is the Functor type class required to be total?  It did not see a total annotation attached to the Functor definition nor did I see the requirement in the idris tutorial.

If so is there anyway to make them partial instead so I can compile the above code?

>Universal quantification = dependent function type. Of course, I don’t believe that is what you want, since it means you get to mention the two arguments everywhere, but you can’t have implicit arguments outside of the top level, so this is all there is.

It is good to see another confirmation that there currently is not equivalent functionality.  That way I can stop spending time on trying to think one up for now.

Patrick

--

You received this message because you are subscribed to the Google Groups "Idris Programming Language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to idris-lang+...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Edwin Brady]

On 22 Jul 2014, at 02:40, Patrick Wheeler <patrick.jo...@gmail.com> wrote:

> This, [1], SO question, commented on by Edwin Brady, probably answers my question (4) for now. It looks like the functionality to easily match Haskell's type synonyms does not yet exist for Idris.
>
> [1] http://stackoverflow.com/q/22880309

Hi Patrick,
I’ve fixed this now, so thought I should wake up this old thread to let you and everyone else know :). I’ve added a proper answer to the question with some examples that might help: http://stackoverflow.com/a/27894091/1125109

This’ll be in the next hackage release, and is in the github master now. I’ve already used it in practice (for a purpose similar to yours, making a type synonym with an implicit argument in an attempt to make Effects more flexible) but naturally more testing would be very useful.

For context: The “this” in question is the ability to have implicit arguments in scopes other than the top level type declarations. The lack of this has been an embarrassment to me for some time but I have only just now had the motivation to get on and do it… I gather a few other people have wanted it too.

There’s still a couple of annoying limitations: pretty printing doesn’t work right yet, and you can’t yet give explicit values to these implicits. Also, scoped type class bindings must be under a scoped implicit - i.e. you can say
a -> ({b : _} -> Show b => …) -> … but not a -> (Show b => …) -> …

These restrictions are mostly just a case of “not implemented yet”/“parser annoyance" so hopefully will be fixed eventually.

Cheers,
Edwin.

[David Christiansen]

Edwin,

> There’s still a couple of annoying limitations: pretty printing doesn’t work right yet, and you can’t yet give explicit values to these implicits. Also, scoped type class bindings must be under a scoped implicit - i.e. you can say
> a -> ({b : _} -> Show b => …) -> … but not a -> (Show b => …) -> …
>
> These restrictions are mostly just a case of “not implemented yet”/“parser annoyance" so hopefully will be fixed eventually.

Would you mind making a Github issue with an example of where the
pretty-printer fails? That way I can take a look and fix it.

/David

[Edwin Brady]

It’s not really a pretty printer issue - the details of what’s implicit aren’t being propagated properly. I’ll finish it off when I get a moment.

Edwin.