2nd bit types in data constructors
I tried to code GADT in PureScript using rank 2 classes as described here for Haskell
My code looks like this:
data Z
data S n
data List a n
= Nil (Z -> n)
| Cons forall m. a (List a m) (S m -> n)
fw :: forall f a. (Functor f) => (forall b . (a -> b) -> f b) -> f a
fw f = f id
bw :: forall f a. (Functor f) => f a -> (forall b . (a -> b) -> f b)
bw x f = map f x
nil :: forall a. List a Z
nil = fw Nil
cons :: forall a n. a -> List a (S n)
cons a as = fw (Cons a as)
instance listFunctor :: Functor (List a) where
map f (Nil k) = Nil (f <<< k)
map f (Cons x xs k) = Cons x xs (f <<< k)
The compiler complains about Wrong number of arguments to constructor Main.Cons
LHS pattern matching in the Functor instance.
What's going on here?
Hello,
Michael
source to share
The syntax used for existential types in Haskell is not present in PureScript. What you wrote for Cons
is a single argument data constructor defined by total.
You may need to use purescript-exists
existential type to encode.
Another option is to use the ultimate painless GADT encoding:
class Listy l where
nil :: forall a. l Z a
cons :: forall a n. a -> l n a -> l (S n) a
You can write conditions for any valid instance Listy
:
myList :: forall l. (Listy l) => l (S (S Z)) Int myList = cons 1 (cons 2 nil)
and interpret them by writing instances
newtype Length n a = Length Int
instance lengthListy :: Listy Length where
nil = Length 0
cons _ (Length n) = Length (n + 1)
newtype AsList n a = AsList (List a)
instance asListListy :: Listy AsList where
nil = AsList Nil
cons x (AsList xs) = AsList (Cons x xs)
source to share