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

[Sergey N. Yashin]

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 <yashin... at gmail.com 
> <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.
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160812/5a099af8/attachment.html>