Re: [Haskell-cafe] Need an example of new type constructor with zero data constructors

12 Aug 2016

      For example empty data declarations, *Fst *and *Snd *in the code bellow:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

module Main where

  data Fst
  data Snd

  data F a b = F b deriving Show
  data S a b = S b deriving Show

  class TupleVal a where
    val :: a b -> b

  instance a ~ Fst => TupleVal (F a) where
    val (F v) = v

  instance a ~ Fst => TupleVal (S a) where
    val (S v) = v

  class TupleOps (a :: * -> * -> *) b c where
    type FST a b c
    type SND a b c
    tfst :: a b c -> FST a b c
    tsnd :: a b c -> SND a b c

  instance (b ~ F b' b'', b' ~ Fst, c ~ S c' c'', c' ~ Snd) => TupleOps (,) 
b c where
    type FST (,) b c = b
    type SND (,) b c = c
    tfst = fst
    tsnd = snd

  instance TupleOps F b (c1, c2) where
    type FST F b (c1, c2) = c1
    type SND F b (c1, c2) = c2
    tfst (F (v1, v2)) = v1
    tsnd (F (v1, v2)) = v2

  instance TupleOps S b (c1, c2) where
    type FST S b (c1, c2) = c1
    type SND S b (c1, c2) = c2
    tfst (S (v1, v2)) = v1
    tsnd (S (v1, v2)) = v2

  type First a = F Fst a
  type Second a = S Snd a

  type a @@ b = (First a, Second b)

  type family a :=: b where
    Fst :=: b = Fst' b
    Snd :=: b = Snd' b

  infixr 1 :=:

  type family Fst' a where
    Fst' (a, b) = a
    Fst' (First a) = Fst' a
    Fst' (Second a) = Fst' a

  type family Snd' a where
    Snd' (a, b) = b
    Snd' (First a) = Snd' a
    Snd' (Second a) = Snd' a

  (@@) :: a -> b -> a @@ b
  a @@ b = (F a, S b)

  tpl1 :: Int @@ String
  tpl1 = 1 @@ "hello"

  tpl2 :: Snd :=: String @@ String
  tpl2 = tsnd ("hello" @@ "world")

  tpl3 :: Snd :=: String @@ String
  tpl3 = tsnd ("hello" @@ "world")

  tpl4 :: Int @@ String
  tpl4 = 1 @@ "hello"

  tpl5 :: Snd :=: String @@ (String @@ String)
  tpl5 = tsnd ("hello" @@ ("hello" @@ "world"))

  tpl6 :: Snd :=: Fst :=: Snd :=: (String @@ String) @@ ((String @@ String) 
@@ String)
  tpl6 = tsnd . tfst . tsnd $ ("world1" @@ "hello2") @@ (("hello3" @@ 
"world5") @@ "world4")

  main :: IO ()
  main = do
    print tpl4
    print tpl3
    print tpl2
    print tpl6

пятница, 12 августа 2016 г., 18:16:18 UTC+3 пользователь James Brown 
написал:
...
What's the purpose to allow data declarations with no constructors?
On Fri, Aug 12, 2016 at 11:08 AM, Sergey N. Yashin javascript:> wrote:
...
For zero data constructors you need to use only EmptyDataDecls 
https://prime.haskell.org/wiki/EmptyDataDecls extension.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.