Partially applied type synonyms

Ttt Mmm

7 Oct 2021 7 Oct '21

10:15 p.m.

I was surprised to find the below code doesn't typecheck even with -XLiberalTypeSynonyms. Am I missing something or is this really not possible? Thanks, Tom --- {-# LANGUAGE FlexibleInstances, KindSignatures, LiberalTypeSynonyms, StandaloneDeriving #-} -- This works: data Foo s x = Foo (s x) x deriving (Eq) -- This replacement doesn't: {- data Foo' sx x = Foo' sx x deriving (Eq) type Foo (s :: * -> *) (x :: *) = Foo' (s x) x -} data Bar (m :: * -> *) = Bar (m Int) -- Neither of these typecheck: x :: Bar (Foo Maybe) x = undefined deriving instance Eq (Bar (Foo Maybe))

Attachments:

attachment.html (text/html — 1.5 KB)

Show replies by date

Branimir Maksimovic

8 Oct 8 Oct

3:18 a.m.

bmaxa@Branimirs-Air haskell % ghc -O2 dtchk.hs Loaded package environment from /Users/bmaxa/.ghc/aarch64-darwin-8.10.7/environments/default [1 of 1] Compiling Main ( dtchk.hs, dtchk.o ) Linking dtchk ... bmaxa@Branimirs-Air haskell % ./dtchk dtchk: Prelude.undefined CallStack (from HasCallStack): error, called at libraries/base/GHC/Err.hs:79:14 in base:GHC.Err undefined, called at dtchk.hs:10:5 in main:Main bmaxa@Branimirs-Air haskell % cat dtchk.hs {-# LANGUAGE FlexibleInstances, KindSignatures, LiberalTypeSynonyms, StandaloneDeriving, FlexibleContexts #-} data Foo sx x = Foo sx x deriving (Eq,Show) data Bar (m :: * -> *) = Bar (m Int) deriving instance Show a => Show (Bar (Foo a)) x :: Bar (Foo (Maybe Int)) x = undefined deriving instance Eq a => Eq (Bar (Foo a)) main = print x Greets, Branimir.

...

On 08.10.2021., at 04:15, Ttt Mmm via Haskell-Cafe wrote:

{-# LANGUAGE FlexibleInstances, KindSignatures, LiberalTypeSynonyms, StandaloneDeriving #-} -- This works: data Foo s x = Foo (s x) x deriving (Eq) -- This replacement doesn't: {- data Foo' sx x = Foo' sx x deriving (Eq) type Foo (s :: * -> *) (x :: *) = Foo' (s x) x -} data Bar (m :: * -> *) = Bar (m Int)

-- Neither of these typecheck: x :: Bar (Foo Maybe) x = undefined deriving instance Eq (Bar (Foo Maybe))

Richard Eisenberg

10:54 a.m.

Hello Tom, Type synonyms must be fully applied. You could try

...

newtype Foo (s :: * -> *) (x :: *) = MkFoo (Foo' (s x) x)

to make something that does not need to be fully applied -- but now you have to worry about the pesky MkFoo constructor. It's hard for me to suggest something else without understanding your use-case better. Sorry! Hope this helps, Richard

...

On Oct 7, 2021, at 10:15 PM, Ttt Mmm via Haskell-Cafe wrote:

I was surprised to find the below code doesn't typecheck even with -XLiberalTypeSynonyms. Am I missing something or is this really not possible?

Thanks, Tom

---

{-# LANGUAGE FlexibleInstances, KindSignatures, LiberalTypeSynonyms, StandaloneDeriving #-} -- This works: data Foo s x = Foo (s x) x deriving (Eq) -- This replacement doesn't: {- data Foo' sx x = Foo' sx x deriving (Eq) type Foo (s :: * -> *) (x :: *) = Foo' (s x) x -} data Bar (m :: * -> *) = Bar (m Int)

-- Neither of these typecheck: x :: Bar (Foo Maybe) x = undefined deriving instance Eq (Bar (Foo Maybe))

_______________________________________________ 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.

Ttt Mmm

7:56 p.m.

...

On 10/08/2021 4:54 PM Richard Eisenberg wrote:

Hello Tom,

Type synonyms must be fully applied. You could try

...
newtype Foo (s :: * -> *) (x :: *) = MkFoo (Foo' (s x) x)

to make something that does not need to be fully applied -- but now you have to worry about the pesky MkFoo constructor.

It's hard for me to suggest something else without understanding your use-case better. Sorry!

Thanks for the suggestions! A newtype is something I'd very much like to avoid due to the wrapping/unwrapping complexity you mention. Here's an example that's hopefully clearer and more motivating; comments inline: {-# LANGUAGE KindSignatures #-} import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set -- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x } x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax data Person m = Person { name :: m String , age :: m Int } person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin } varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag)) -- So far so good. But what if you want to define a version of 'Var' that uses 'IntSet' internally? -- An attempt would be to comment out the definition of 'Var' above and instead say: {- data Var' sx x = Var { xs :: sx , getX :: sx -> Maybe x } type Var s x = Var' (s x) x y :: Var' IntSet Int y = Var (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView) -} -- 'varMay' works with a generalized type signature (though I don't need it to have one): -- varMay :: Person (Var' sx) -> Person Maybe -- But I can't define 'person0' -- To be clear, I think I can understand why e.g. a type synonym wouldn't work, but i can't find something that would work in its place

...

Hope this helps, Richard

...
On Oct 7, 2021, at 10:15 PM, Ttt Mmm via Haskell-Cafe wrote:

I was surprised to find the below code doesn't typecheck even with -XLiberalTypeSynonyms. Am I missing something or is this really not possible?

Thanks, Tom

---

{-# LANGUAGE FlexibleInstances, KindSignatures, LiberalTypeSynonyms, StandaloneDeriving #-} -- This works: data Foo s x = Foo (s x) x deriving (Eq) -- This replacement doesn't: {- data Foo' sx x = Foo' sx x deriving (Eq) type Foo (s :: * -> *) (x :: *) = Foo' (s x) x -} data Bar (m :: * -> *) = Bar (m Int)

-- Neither of these typecheck: x :: Bar (Foo Maybe) x = undefined deriving instance Eq (Bar (Foo Maybe))

_______________________________________________ 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.

Branimir Maksimovic

10:14 p.m.

{-# LANGUAGE KindSignatures,FlexibleInstances #-} import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set import Maybes -- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x } x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax data Person m = Person { name :: m String , age :: m Int } person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin } varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag)) instance Show (Var' IntSet Int) where show (Var' a b) = show a data Var' a b = Var'{ xs' :: a ,getX' :: a -> Maybe b } y :: Var' IntSet Int y = Var' (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView) main = print y

...

On 09.10.2021., at 01:56, Ttt Mmm via Haskell-Cafe wrote:

{-# LANGUAGE KindSignatures #-}

import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set

-- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x }

x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax

data Person m = Person { name :: m String , age :: m Int }

person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin }

varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag))

-- So far so good. But what if you want to define a version of 'Var' that uses 'IntSet' internally?

-- An attempt would be to comment out the definition of 'Var' above and instead say: {- data Var' sx x = Var { xs :: sx , getX :: sx -> Maybe x }

type Var s x = Var' (s x) x

y :: Var' IntSet Int y = Var (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView) -}

Ttt Mmm

9 Oct 9 Oct

1:04 a.m.

...

On 10/09/2021 4:14 AM Branimir Maksimovic wrote:

{-# LANGUAGE KindSignatures,FlexibleInstances #-}

import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set import Maybes -- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x }

x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax

data Person m = Person { name :: m String , age :: m Int }

person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin }

varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag))

instance Show (Var' IntSet Int) where show (Var' a b) = show a data Var' a b = Var'{ xs' :: a ,getX' :: a -> Maybe b } y :: Var' IntSet Int y = Var' (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView)

Thanks for this suggestion, but here Var' is defined as a totally separate type than Var, whereas I want/need Var to be defined in terms of Var'. Cheers, Tom

...

main = print y

> > On 09.10.2021., at 01:56, Ttt Mmm via Haskell-Cafe wrote:

...
{-# LANGUAGE KindSignatures #-}

import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set

-- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x }

x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax

data Person m = Person { name :: m String , age :: m Int }

person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin }

varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag))

-- So far so good. But what if you want to define a version of 'Var' that uses 'IntSet' internally?

-- An attempt would be to comment out the definition of 'Var' above and instead say: {- data Var' sx x = Var { xs :: sx , getX :: sx -> Maybe x }

type Var s x = Var' (s x) x

y :: Var' IntSet Int y = Var (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView) -}

>

Branimir Maksimovic

2:25 a.m.

...

On 09.10.2021., at 07:04, Ttt Mmm wrote:

...
On 10/09/2021 4:14 AM Branimir Maksimovic wrote:

{-# LANGUAGE KindSignatures,FlexibleInstances #-}

import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set import Maybes -- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x }

x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax

data Person m = Person { name :: m String , age :: m Int }

person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin }

varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag))

instance Show (Var' IntSet Int) where show (Var' a b) = show a data Var' a b = Var'{ xs' :: a ,getX' :: a -> Maybe b } y :: Var' IntSet Int y = Var' (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView)

Thanks for this suggestion, but here Var' is defined as a totally separate type than Var, whereas I want/need Var to be defined in terms of Var'.

Why, what do mean by that? they are unrelated types as IntSet has one var less then Set?

...

Cheers, Tom

Greets, Branimir,

...

...
main = print y

...
On 09.10.2021., at 01:56, Ttt Mmm via Haskell-Cafe mailto:haskell-cafe@haskell.org> wrote:

{-# LANGUAGE KindSignatures #-}

import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set

-- Start with this definition: data Var s x = Var { xs :: s x , getX :: s x -> Maybe x }

x :: Var Set Double x = Var (Set.fromList [1,2,3]) Set.lookupMax

data Person m = Person { name :: m String , age :: m Int }

person0 :: Person (Var Set) person0 = Person { name = Var (Set.fromList ["alice", "bob"]) Set.lookupMin , age = Var (Set.fromList [20,30]) Set.lookupMin }

varMay :: Person (Var Set) -> Person Maybe varMay (Person nm ag) = Person (getX nm (xs nm)) (getX ag (xs ag))

-- So far so good. But what if you want to define a version of 'Var' that uses 'IntSet' internally?

-- An attempt would be to comment out the definition of 'Var' above and instead say: {- data Var' sx x = Var { xs :: sx , getX :: sx -> Maybe x }

type Var s x = Var' (s x) x

y :: Var' IntSet Int y = Var (IntSet.fromList [1,2,3]) (fmap fst . IntSet.minView) -}

1323

Age (days ago)

1324

Last active (days ago)

List overview

Download

6 comments

3 participants

participants (3)

Branimir Maksimovic
Richard Eisenberg
Ttt Mmm