0
{-# LANGUAGE RankNTypes, ScopedTypeVariables, NoMonomorphismRestriction #-}

type CList a = (forall t . (a -> t -> t) -> t -> t)

ccons :: forall a . a -> CList a -> CList a
ccons h t = (\ c n -> c h (t c n))

cnil :: forall h . CList h
cnil = (\ c n -> n)

cToList :: forall a . CList a -> [a]
cToList list = list (:) []

cFromList :: forall a . [a] -> CList a
cFromList = foldr ccons cnil

main = print (cToList (cFromList [1,2,3]))

I understand the reason it doesn't compile has to do with the usage of forall on ccons. Commenting the ccons type will make it compile, but with an awkward type for ccons. What is the right way to fix it?

test.hs:15:23:
    Couldn't match type ‘(a -> t -> t) -> t -> t’
                   with ‘forall t1. (a -> t1 -> t1) -> t1 -> t1’
    Expected type: a
                   -> ((a -> t -> t) -> t -> t) -> (a -> t -> t) -> t -> t
      Actual type: a -> CList a -> (a -> t -> t) -> t -> t
    Relevant bindings include
      cFromList :: [a] -> CList a (bound at test.hs:15:5)
    In the first argument of ‘foldr’, namely ‘ccons’
    In the expression: foldr ccons cnil
jub0bs
  • 60,866
  • 25
  • 183
  • 186
MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
  • Actually, the issue isn't with `forall`. It's actually saying that the `t` in your `ccons` function is different from the `t` in your `cFromList` function. Hence the `t` and `t1` business. – Kwarrtz Feb 04 '16 at 02:35
  • Yes, but can I fix it somehow? – MaiaVictor Feb 04 '16 at 02:51
  • 1
    I feel so sure that you've asked something really similar to this before and got told to use `newtype` instead of `type` (which should do fine as a solution here, too), but I can't find the question now... – Daniel Wagner Feb 04 '16 at 02:58
  • Impredicativity bites. – dfeuer Feb 04 '16 at 03:10
  • @DanielWagner sorry, I probably did, but I ask so much and do so much work in parallel that it is almost impossible even for myself to keep track of my own legacy :( I wish I could just stop, sit and learn instead of living like that. Oh well – MaiaVictor Feb 04 '16 at 03:37
  • Are you sure you aren't confusing for when I asked about the **Scott** encoding? I was told I need `newtype` instead of `type` for it to work [and it does indeed](http://lpaste.net/151650)... that's all I remember, though. Couldn't find anything that looks like the answer to this question googling for myself. Maybe I'm just not making the connection. Sorry :( – MaiaVictor Feb 04 '16 at 03:45
  • Basically, if you introduce a new rank-n-type, wrap it in `newtype`. – effectfully Feb 04 '16 at 04:03

2 Answers2

3

Why are you using ccons at all? cFromList is just a flipped foldr

cFromList ::  [a] -> CList a
cFromList xs op seed = foldr op seed xs
Michael
  • 2,889
  • 17
  • 16
  • Oh. Or that, lol. Thanks. (Is there any problem in not using `newtype`, though? I don't quite understand well the source of this problem - I don't know if it will break something later on or if there will always be an obvious solution like this one.) – MaiaVictor Feb 04 '16 at 03:58
  • 1
    Newtyping the Church encoding will have a number of advantages. It will make type messages more intelligible and will permit, e.g. Functor and Monad instances and so on. – Michael Feb 04 '16 at 04:00
  • I think usually when I have done things like this and 'really' just wanted the rank-2 type, I would also keep the newtyped version around to use when I couldn't get the compiler to grasp my meaning. – Michael Feb 04 '16 at 04:05
  • 2
    @Viclib, all sorts of things with go wonky without the `newtype`. All your `forall`s will get shoved as far to the left as possible. A `newtype` will block `forall` migration so you can get results as polymorphic as you need. There will surely be other reasons too. – dfeuer Feb 04 '16 at 06:26
2

As pointed by @Daniel Wagner, merely using newtype instead of type solves the issue:

newtype CList a = CList { runCList :: (forall t . (a -> t -> t) -> t -> t) }

ccons :: forall h . h -> CList h -> CList h
ccons h t = CList (\ c n -> c h (runCList t c n))

cnil :: forall h . CList h
cnil = CList (\ c n -> n)

cToList :: forall a . CList a -> [a]
cToList list = runCList list (:) []

cFromList :: forall a . [a] -> CList a
cFromList list = (foldr ccons cnil list)

main = print (cToList (cFromList [1,2,3]))

Also apparently I was told this before but I really can not remember nor find the question. Sorry guys :(

MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
  • [That's the one](http://stackoverflow.com/questions/31931432/is-it-possible-to-use-church-encodings-without-breaking-equational-reasoning/31942453#31942453) – gallais Feb 04 '16 at 13:51
  • @gallais oh I even read that one before... so I guess I was too stupid to notice they were related. – MaiaVictor Feb 05 '16 at 13:22