Skip to content

forall

--Copyright (C) 2017  Zaoqi

--This program is free software: you can redistribute it and/or modify
--it under the terms of the GNU Affero General Public License as published
--by the Free Software Foundation, either version 3 of the License, or
--(at your option) any later version.

--This program is distributed in the hope that it will be useful,
--but WITHOUT ANY WARRANTY; without even the implied warranty of
--MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--GNU Affero General Public License for more details.

--You should have received a copy of the GNU Affero General Public License
--along with this program.  If not, see <http://www.gnu.org/licenses/>.
{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs,
MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes,
UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction,
ScopedTypeVariables #-}

module Data.U where

data U :: [*] -> * where
    UOne :: x -> U (x : xs)
    USucc :: U xs -> U (x : xs)

class Usuccs a b where
    usuccs :: U a -> U b
instance Usuccs a a where
    usuccs = id
instance Usuccs xs ys => Usuccs (x : xs) (x : ys) where
    usuccs (UOne x) = UOne x
    usuccs (USucc xs) = USucc (usuccs xs)
instance Usuccs xs (x : xs) where
    usuccs = USucc
instance Usuccs xs ys => Usuccs xs (y : ys) where
    usuccs x = USucc (usuccs x)

u :: forall x xs. Usuccs '[x] xs => x -> U xs
u x = usuccs (UOne x :: U '[x])

class T a b where
    t :: U a -> U b
instance Usuccs '[x] t => T '[x] t where
    t (UOne x) = u x
instance (T xs t, Usuccs '[x] t) => T (x ': xs) t where
    t (UOne x) = u x
    t (USucc xs) = t xs

instance Eq x => Eq (U '[x]) where
    UOne x == UOne y = x == y
instance (Eq x, Eq (U xs)) => Eq (U (x : xs)) where
    UOne x == UOne y = x == y
    USucc xs == USucc ys = xs == ys
    _ == _ = False

instance Show x => Show (U '[x]) where
    show (UOne x) = "(u " ++ showsPrec 11 x ")"
instance (Show x, Show (U xs)) => Show (U (x : xs)) where
    show (UOne x) = "(u " ++ showsPrec 11 x ")"
    show (USucc xs) = show xs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Prelude> :load U.hs 
[1 of 1] Compiling Data.U           ( U.hs, interpreted )
Ok, modules loaded: Data.U.
*Data.U> :t u
u :: Usuccs '[x] xs => x -> U xs
--Copyright (C) 2017  Zaoqi

--This program is free software: you can redistribute it and/or modify
--it under the terms of the GNU Affero General Public License as published
--by the Free Software Foundation, either version 3 of the License, or
--(at your option) any later version.

--This program is distributed in the hope that it will be useful,
--but WITHOUT ANY WARRANTY; without even the implied warranty of
--MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--GNU Affero General Public License for more details.

--You should have received a copy of the GNU Affero General Public License
--along with this program.  If not, see <http://www.gnu.org/licenses/>.
{-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs,
MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, AllowAmbiguousTypes,
UndecidableInstances, IncoherentInstances, NoMonomorphismRestriction,
ScopedTypeVariables #-}

module Data.U where

data U :: [*] -> * where
    UOne :: x -> U (x : xs)
    USucc :: U xs -> U (x : xs)

class Usuccs a b where
    usuccs :: U a -> U b
instance Usuccs a a where
    usuccs = id
instance Usuccs xs ys => Usuccs (x : xs) (x : ys) where
    usuccs (UOne x) = UOne x
    usuccs (USucc xs) = USucc (usuccs xs)
instance Usuccs xs (x : xs) where
    usuccs = USucc
instance Usuccs xs ys => Usuccs xs (y : ys) where
    usuccs x = USucc (usuccs x)

u :: Usuccs '[x] xs => x -> U xs
u x = usuccs (UOne x :: U '[x])

class T a b where
    t :: U a -> U b
instance Usuccs '[x] t => T '[x] t where
    t (UOne x) = u x
instance (T xs t, Usuccs '[x] t) => T (x ': xs) t where
    t (UOne x) = u x
    t (USucc xs) = t xs

instance Eq x => Eq (U '[x]) where
    UOne x == UOne y = x == y
instance (Eq x, Eq (U xs)) => Eq (U (x : xs)) where
    UOne x == UOne y = x == y
    USucc xs == USucc ys = xs == ys
    _ == _ = False

instance Show x => Show (U '[x]) where
    show (UOne x) = "(u " ++ showsPrec 11 x ")"
instance (Show x, Show (U xs)) => Show (U (x : xs)) where
    show (UOne x) = "(u " ++ showsPrec 11 x ")"
    show (USucc xs) = show xs
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Prelude> :load U.hs 
[1 of 1] Compiling Data.U           ( U.hs, interpreted )

U.hs:39:7: error:
    • Could not deduce (Usuccs '[x0] xs) arising from a use of ‘usuccs’
      from the context: Usuccs '[x] xs
        bound by the type signature for:
                   u :: Usuccs '[x] xs => x -> U xs
        at U.hs:38:1-32
      The type variable ‘x0’ is ambiguous
      Relevant bindings include u :: x -> U xs (bound at U.hs:39:1)
    • In the expression: usuccs (UOne x :: U '[x])
      In an equation for ‘u’: u x = usuccs (UOne x :: U '[x])

U.hs:39:15: error:
    • Couldn't match type ‘x’ with ‘x1’
      ‘x’ is a rigid type variable bound by
        the type signature for:
          u :: forall x (xs :: [*]). Usuccs '[x] xs => x -> U xs
        at U.hs:38:6
      ‘x1’ is a rigid type variable bound by
        an expression type signature:
          forall x1. U '[x1]
        at U.hs:39:25
      Expected type: U '[x1]
        Actual type: U '[x]
    • In the first argument of ‘usuccs’, namely ‘(UOne x :: U '[x])’
      In the expression: usuccs (UOne x :: U '[x])
      In an equation for ‘u’: u x = usuccs (UOne x :: U '[x])
    • Relevant bindings include
        x :: x (bound at U.hs:39:3)
        u :: x -> U xs (bound at U.hs:39:1)
Failed, modules loaded: none.
Trac metadata
Trac field Value
Version 8.0.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information