jchia_ 2017-02-01 19:45:16
yes, that allows catching as SomeException or as IOError
ski 2017-02-01 19:45:21
(`M' of type `A', `N' of type `B', `(M,N)' getting type `A * B')
jle` 2017-02-01 19:45:37
jchia_: the implementation is actually in the docts i think
jle` 2017-02-01 19:45:54
ah yeah it's right there
mniip 2017-02-01 19:45:57
jchia_, I think that might go all the way into the RTS
ski 2017-02-01 19:46:19
if `M' is a term of type `A -> B', and `N' a term of type `A', then `M $ N', aka `apply (M,N)' is a term of type `B'
jle` 2017-02-01 19:46:35
actually nvm i'm not sure what the question is exactly
ski 2017-02-01 19:46:37
(`apply' is a morphism from `(A -> B) * A' to `B')
mniip 2017-02-01 19:46:40
ski, okay I can agree with that
jle` 2017-02-01 19:46:46
nothing about the Exception system in haskell is magic
jle` 2017-02-01 19:46:56
it could have been implemented in scratch within the language
mniip 2017-02-01 19:47:07
but is '\x |-> something that is a term when x is a term' a term?
jle` 2017-02-01 19:47:22
so exceptions doesn't require any magical language/ghc hacking to work
ski 2017-02-01 19:47:42
the sub-term has free variables with types as in the context `f : A * B -> C,x : A,y : B'
ski 2017-02-01 19:48:27
in my case, since i'm using only binary products, i actually need to distinguish the grouping in the context, in this case it should be `(f : A * B -> C,x : A),y : B'
mniip 2017-02-01 19:49:06
what the hell is a free variable
ski 2017-02-01 19:49:15
so, the term `f $ (x,y)', as well as the sub-terms `(f,(x,y))',`f',`(x,y)',`x',`y' are all typed in this context
mniip 2017-02-01 19:49:16
no like I understand what it is
jchia_ 2017-02-01 19:49:26
jle`: The magic I refer to is that the catching seems to be too permissive about type matching. How come an IOError automatically 'becomes' a SomeException when I want to catch it as such?
mniip 2017-02-01 19:49:37
but what do our terms have to do with a formal system's terms
ski 2017-02-01 19:49:50
every term comes with a context describing the names and types of the variables which *may* appear free in it
jle` 2017-02-01 19:50:01
jchia_: i think you can implement that too using Typeable machinery
jchia_ 2017-02-01 19:50:08
jle`: Can that be implemented using pure haskell or does that require special-casing in the language or RTS?
ski 2017-02-01 19:50:09
our terms *are* formal terms
jle` 2017-02-01 19:50:20
jchia_: the thing doing the work there is probably 'catch'/'handle'
jle` 2017-02-01 19:50:30
that's...my suspicion
ski 2017-02-01 19:50:33
because the current context is `(f : A * B -> C,x : A),y : B'
mniip 2017-02-01 19:50:44
ski, wait
mniip 2017-02-01 19:50:55
when did that happen
jle` 2017-02-01 19:51:18
jchia_: i...might want to try it out myself before claiming this
ski 2017-02-01 19:51:34
i'm starting from the inside, so i'm just claiming that the current context is that thing
ski 2017-02-01 19:51:54
you'll see that it works, when we reach the outside, the root of the whole term
ski 2017-02-01 19:52:09
one could do it from outside-to-inside, but it's a little bit harder to follow
ski 2017-02-01 19:52:13
`y' is translated into `snd' (a morphism from `((A * B -> C) * A) * B' to `B', here)
ski 2017-02-01 19:52:37
`x' is translated into `snd . fst' (a morphism from `((A * B -> C) * A) * B' to `A')
halogenandtoast 2017-02-01 19:52:56
I have some code that looked like `f <$> map g <$> h x` and I thought it might look nicer to swap the order so I wrote a function that is essentially `<$$> = flip (<$>)` so I can do `h x <$$> map g <$$> f` but I don't like having to add a new operator like this. Is there already a built in way of handling this?
ski 2017-02-01 19:53:09
and `f' is translated into `fst . fst (a morphism from `((A * B -> C) * A) * B' to `A * B -> C')
mniip 2017-02-01 19:53:23
ski, you're running away :(
ski 2017-02-01 19:53:52
so, what's happening here is that we go from the typing judgement `Gamma |- y : B', where `Gamma' is the context `(f : A * B -> C,x : A),y : B
ski 2017-02-01 19:53:55
'
jle` 2017-02-01 19:54:51
halogenandtoast: there's <**>, which doesn't flip the order of effects
jle` 2017-02-01 19:55:16
but also there has been talks about a standardized flip (<$>). some libaries export their own version, like <&>
ski 2017-02-01 19:55:18
into the morphism `snd : ((A * B -> C) * A) * B >---> B', by erasing all the names from the context, replacing `,'s by `*', and using a composition of `fst' and `snd' to select the compoenent of the nested product type which corresponds to the variable
halogenandtoast 2017-02-01 19:55:31
jle`: but that's `f a -> f (a -> b) -> f b` but I wan't `f a -> (a -> b) -> f b`
halogenandtoast 2017-02-01 19:55:36
*want
mniip 2017-02-01 19:55:37
ski, when did we go from abstract term things to formal terms
ski 2017-02-01 19:56:07
mniip : so, i'm currently attempting to explain how we translate terms which are variables (as opposed to morphism applications, or pairs, or lambdas)
jle` 2017-02-01 19:56:12
but your first function is just 'f . map g <$> h x', maybe that's clenaer?
ski 2017-02-01 19:56:16
mniip : what's the difference ?
halogenandtoast 2017-02-01 19:56:44
jle`: yeah that might be cleaner, trying that out
jle` 2017-02-01 19:56:46
using <&> i'd be h x <&> map g <&> f, maybe, but, gross
mniip 2017-02-01 19:57:04
the first we defined to be inhabitans of objects in our category
jle` 2017-02-01 19:57:11
the main reason i've usually wanted <&> is to make it easy to write multi-line lambdas as your mapping function
halogenandtoast 2017-02-01 19:57:15
jle`: nice catch with (.)
mniip 2017-02-01 19:57:29
the latter is an inductively defined string of symbols?
jle` 2017-02-01 19:57:30
but in your case you're actually flipping the order of function application, which is typically frowned upon
dram_phone 2017-02-01 19:57:49
Sorry, I was disconnected and never noticed
jle` 2017-02-01 19:57:51
no problem! the second functor law is basically (<$>) = (.)
jle` 2017-02-01 19:58:00
(it's not, that was a joke)
ski 2017-02-01 19:58:05
mniip : the internal language is a (formal) language for describing morphisms, by means of describing "inhabitants of objects" (regardless of whether they "exist" or not)
dram_phone 2017-02-01 19:58:15
@let type UEither = forall m. Either m
lambdabot 2017-02-01 19:58:17
Defined.
halogenandtoast 2017-02-01 19:58:20
jle`: it is for functions though right?
dram_phone 2017-02-01 19:58:23
:k UEither
lambdabot 2017-02-01 19:58:25
* -> *
mniip 2017-02-01 19:58:29
I sense circular reasoning
dram_phone 2017-02-01 19:58:57
Question: why does '(forall m. ...) :: * -> *' make sense?
ski 2017-02-01 19:59:02
mniip : i'd rather forget about the "string" part there. make it an inductively defined tree, up to renaming of bound variables
dram_phone 2017-02-01 19:59:08
IIUC it doesn't work in, say, Coq
jle` 2017-02-01 19:59:16
halogenandtoast: yeah, it is
jle` 2017-02-01 19:59:29
but the way i was using it was to imply that it's the case for all functors
mniip 2017-02-01 19:59:33
right
jle` 2017-02-01 19:59:35
f <$> g <$> x = f . g <$> x
halogenandtoast 2017-02-01 19:59:35
Right
mniip 2017-02-01 19:59:36
that works too
ski 2017-02-01 19:59:53
dram_phone : apparently `forall' is lifted so that `(forall x. ..x..) a' means `forall x. (..x..) a
ski 2017-02-01 19:59:56
'
jle` 2017-02-01 20:00:34
another way of stating the functor laws is that <$> is associative
dram_phone 2017-02-01 20:00:41
> join (Right (Right 4) :: UEither (UEither Int))
halogenandtoast 2017-02-01 20:00:42
jle`: thanks for the help, I'll avoid swapping order of function application in the future.
lambdabot 2017-02-01 20:00:43
error:
lambdabot 2017-02-01 20:00:43
• Illegal polymorphic type: forall m. Either m
lambdabot 2017-02-01 20:00:43
GHC doesn't yet support impredicative polymorphism
jle` 2017-02-01 20:00:45
f <$> (g <$> x) = (f <$> g) <$> x
jle` 2017-02-01 20:00:49
^^
halogenandtoast 2017-02-01 20:00:59
Right
dram_phone 2017-02-01 20:01:22
ski: is it? That gets interesting
ski 2017-02-01 20:01:25
mniip : anyway, i'd rather also forget about "the first we defined to be inhabitans of objects in our category", since the way we defined our category, our objects might not be sets/types at all
mniip 2017-02-01 20:01:33
right
mniip 2017-02-01 20:01:44
I have no idea how we defined terms then
jle` 2017-02-01 20:01:49
halogenandtoast: no problem!
ski 2017-02-01 20:01:51
mniip : what the internal language does is that it allows us to *pretend* that our objects have inhabitants, in a nice way
dram_phone 2017-02-01 20:03:18
It just, just makes no sense to me
ski 2017-02-01 20:03:19
@type let uRight :: a -> UEither a; uRight = Right in uRight -- ah ah :)
mniip 2017-02-01 20:03:20
ski, ok so you propose that all operations that can be done on FOL terms can be done on morphisms too?
lambdabot 2017-02-01 20:03:21
error:
lambdabot 2017-02-01 20:03:21
• Illegal polymorphic type: forall m. Either m
lambdabot 2017-02-01 20:03:21
GHC doesn't yet support impredicative polymorphism
ski 2017-02-01 20:03:39
presumably with impredicative types enabled, that'd work ?
dram_phone 2017-02-01 20:03:49
I hope!
ski 2017-02-01 20:04:42
mniip : we have term variables, we have pairing of terms, we have application of a morphism to a term, we have lambda-abstraction of a term wrt a variable
dram_phone 2017-02-01 20:06:03
ski: In a way, when impredicative is enabled, you're wrong
dram_phone 2017-02-01 20:06:06
https://glot.io/snippets/emqzrmowx1
ski 2017-02-01 20:06:18
mniip : the morphisms that occur in terms here are typically taken to be any morphism you like in the category
jle` 2017-02-01 20:06:24
jchia_: looked at it again and, yeah, it looks like you can implement the behavior you're talking about in plain haskell
dram_phone 2017-02-01 20:06:35
Well...
jle` 2017-02-01 20:06:38
jchia_: or, i mean, within GHC haskell
ski 2017-02-01 20:06:47
dram_phone : "In a way" ?
dram_phone 2017-02-01 20:07:04
Either (no pun intended) you're wrong or I misunderstood something terribly
jle` 2017-02-01 20:07:13
jchia_: the 'magic' comes from 'fromException :: Exception e => SomeException -> Maybe e', which is a part of the Exception typeclass, and every instance implements it
jle` 2017-02-01 20:07:22
jchia_: so it boils down to return-type polymorphism
dram_phone 2017-02-01 20:07:34
No instance for (Monad (forall m. Either m))
mniip 2017-02-01 20:07:36
ski, so we're coming up with names for morphisms in a way that lets us correctly reason about morphism equality?
jle` 2017-02-01 20:07:51
jchia_: 'catch' dispatches the fromException implementation for the type you want to catch. Sometimes, 'fromException' might return Just for more than one instance
ski 2017-02-01 20:08:17
mniip : i suppose so. or just talk about morphisms, as constructed "in terms of mappings of inhabitants"
mniip 2017-02-01 20:08:22
like that if you compose the morphism named "x |-> x + 1" with one named "x |-> x + 2" you get one named "x |-> x + 3"
jle` 2017-02-01 20:08:26
jchia_: for example, both the instance for SomeException and the instance for IOException would return 'Just', if given an IOException in a SomeException constructor
jchia_ 2017-02-01 20:08:32
jle`: What is return-type polymorphism?
jchia_ 2017-02-01 20:09:01
jle`: An extension, a technique, something els?
jle` 2017-02-01 20:09:03
> return 10 :: [Int]
lambdabot 2017-02-01 20:09:05
[10]
jle` 2017-02-01 20:09:10
> mempty :: String
dram_phone 2017-02-01 20:09:11
type variable on the right side of an arrow
lambdabot 2017-02-01 20:09:12
""
jle` 2017-02-01 20:09:17
> return 10 :: Maybe Int
lambdabot 2017-02-01 20:09:19
Just 10
dram_phone 2017-02-01 20:09:32
Actually, screw that 'return type polymorphism' thing
mniip 2017-02-01 20:09:38
ski, alright, I can kind of see the reasoning behind it now
mniip 2017-02-01 20:09:55
but
dram_phone 2017-02-01 20:10:01
jchia_: technique
jle` 2017-02-01 20:10:05
jchia_: the instance of 'Monad' or 'Monoid' chosen depends on the expected type of the result
ski 2017-02-01 20:10:07
jle` : imho "Sometimes, 'fromException' might return Just for more than one instance" sounds .. weird
mniip 2017-02-01 20:10:07
I'm not at all sure about the theorem of deduction in such a formal system
jle` 2017-02-01 20:10:29
ski: er, the phrasing might be a bit weird yeah
dram_phone 2017-02-01 20:11:22
I thought we've got an oop-like exception type hierarchy available
dram_phone 2017-02-01 20:11:31
Through dynamic typinf
dram_phone 2017-02-01 20:11:34
*typing
mniip 2017-02-01 20:11:50
haha no
jle` 2017-02-01 20:11:57
i guess i mean that, for a given value of type SomeException...more than one instance of Exception's fromException implementation might return a Just when given that SomeException
mniip 2017-02-01 20:11:58
exceptions are both black magic and awkward to use
ski 2017-02-01 20:11:59
mniip : as usual in natural deduction (or sequent calculus), that "theorem" is a basic inference rule, so holds trivially
ski 2017-02-01 20:12:29
jle` : no, i meant that what you described always has come off as weird to me .. not the way you described it in
jle` 2017-02-01 20:12:38
i mean, it's the case for Read
jle` 2017-02-01 20:12:43
> read "1.52" :: Double
lambdabot 2017-02-01 20:12:45
1.52
dram_phone 2017-02-01 20:12:46
Exceptions are literally for 'just f**k it' situations
jle` 2017-02-01 20:12:54
> readMaybe "1.52" :: Maybe Double
lambdabot 2017-02-01 20:12:56
error:
lambdabot 2017-02-01 20:12:56
Variable not in scope: readMaybe :: [Char] -> Maybe Double
ski 2017-02-01 20:13:00
dram_phone : i disagree
jle` 2017-02-01 20:13:03
@let import Text.Read
lambdabot 2017-02-01 20:13:05
Defined.
jle` 2017-02-01 20:13:06
> readMaybe "1.52" :: Maybe Float
lambdabot 2017-02-01 20:13:09
Just 1.52
jle` 2017-02-01 20:13:11
> readMaybe "1.52" :: Maybe Double
lambdabot 2017-02-01 20:13:13
Just 1.52
jle` 2017-02-01 20:13:31
exceptions are actually a very focused and disciplined tool with a concrete use case, so they're not that bad
jchia_ 2017-02-01 20:13:37
jle`: So, that's what you mean by "return-type" polymorphism, right?
jle` 2017-02-01 20:13:59
yeah, return type polymorphism is how 'fromException' works
jle` 2017-02-01 20:14:13
and 'catch' uses that to implement its "catch you what you want" behavior
jle` 2017-02-01 20:14:35
in the above case, "1.52" is 'read' by both Float's instance and Double's instance
ski 2017-02-01 20:14:37
> cast (2 :: Int) :: Maybe Int
lambdabot 2017-02-01 20:14:40
Just 2
ski 2017-02-01 20:14:40
> cast (2 :: Int) :: Maybe Integer
lambdabot 2017-02-01 20:14:42
Nothing
ski 2017-02-01 20:14:46
is another example
dram_phone 2017-02-01 20:15:08
ski: Uh
jle` 2017-02-01 20:15:12
and say, a value of type IOException can be fromException'd by both SomeException's instance and IOException's instance
dram_phone 2017-02-01 20:15:15
I wasn't serious sorry
jle` 2017-02-01 20:15:32
or i can give an example with concrete values
jle` 2017-02-01 20:15:40
> fromException Overflow :: Maybe SomeException
lambdabot 2017-02-01 20:15:42
error:
lambdabot 2017-02-01 20:15:42
• Couldn't match expected type 'SomeException'
lambdabot 2017-02-01 20:15:42
with actual type 'ArithException'
dram_phone 2017-02-01 20:15:50
note to self: no joking about random things
jle` 2017-02-01 20:15:54
> fromException (SomeException Overflow) :: Maybe SomeException
lambdabot 2017-02-01 20:15:57
Just arithmetic overflow
jle` 2017-02-01 20:16:03
> fromException (SomeException Overflow) :: Maybe ArithException
lambdabot 2017-02-01 20:16:05
Just arithmetic overflow
jle` 2017-02-01 20:16:22
both the SomeException instance and the ArithException instance can 'fromException' the (SomeException Overflow) value
jle` 2017-02-01 20:16:28
> fromException (SomeException Overflow) :: Maybe IOException
lambdabot 2017-02-01 20:16:31
Nothing
ski 2017-02-01 20:17:38
> case fromException (SomeException Overflow) of Just exn -> case fromException exn of Just Overflow -> () -- imho, this is very weird
lambdabot 2017-02-01 20:17:40
()
dram_phone 2017-02-01 20:18:09
this is very dynamic typing
romano 2017-02-01 20:18:35
hi guys
jle` 2017-02-01 20:18:40
the semantics are a bit weird, yes. but the mechanics are kinda plain
mniip 2017-02-01 20:18:43
> iterate (fromJust . fromException) (SomeException Overflow)
lambdabot 2017-02-01 20:18:45
[arithmetic overflow,arithmetic overflow,arithmetic overflow,arithmetic over...
jle` 2017-02-01 20:18:50
the original question was about the mechanics of how it was implemented
jchia_ 2017-02-01 20:19:11
jle`: I got it. Thanks.
jle` 2017-02-01 20:19:12
but yeah, the semantics that the Exception class implements is arguably odd
ski 2017-02-01 20:19:20
`toException' shouldn't be idempotent, is my feeling
dram_phone 2017-02-01 20:19:22
I thought it was Typeable
jle` 2017-02-01 20:19:57
typeable and existential types, yeah
jle` 2017-02-01 20:20:03
but not a particularly magical use of either
romano 2017-02-01 20:20:29
i have a few io computations that return values or errors. at the moment i simply throw an exception if there is an error but i'd like to encode this in the type signatures. i thought of using ExceptT but i read somewhere that it's an anti-pattern. is there a recommended way to do this?
jle` 2017-02-01 20:21:14
romano: you should use exceptions if the the error comes from IO errors, or asynchronous errors
jle` 2017-02-01 20:21:53
you can probably just return an (Either e a) if you have a 'pure' error, like for math or a data type operation or something
jle` 2017-02-01 20:23:20
the only difference between an ExceptT e IO a and an IO (Either e a) is a newtype wrapping/unwrapping
romano 2017-02-01 20:23:35
jle`, these errors are not strictly pure but they are expected so i don't think exceptions fit here
jle` 2017-02-01 20:24:13
a reasonable Either might be a file is read properly, but the contents are not parsed
ski 2017-02-01 20:24:22
romano : what does "not strictly pure" and "expected" mean here ?
jle` 2017-02-01 20:24:38
you could probably have that as an IO (Either ParseError a)
jle` 2017-02-01 20:24:56
and the actual IO errors (like file not found, etc.) would come out as exceptions
jle` 2017-02-01 20:25:16
the difference between IO (Either e a) and ExceptT e IO a is probably just convenience at the call site
romano 2017-02-01 20:25:17
ski, e.g. the computation downloads a url successfully but doesn't find useful data in it
jle` 2017-02-01 20:25:20
call site(s)
ski 2017-02-01 20:25:49
romano : sounds like the situation jle` is talking about, then
dram_phone 2017-02-01 20:26:04
romano: Is that often expected?
dram_phone 2017-02-01 20:26:22
Can the program reasonably continue after such an error?
jle` 2017-02-01 20:26:45
it's a bit of a judgment call, but i'd go with IO (Either e a) for that. url not found would be an exception, and the Either would handle how the data is processed
romano 2017-02-01 20:26:47
dram_phone, no, it cannot. it's part of input validation
dram_phone 2017-02-01 20:27:21
just, if you literally catch the exception at each use site it's not good
dram_phone 2017-02-01 20:27:30
(Looking at you, KeyError!)
jle` 2017-02-01 20:27:36
but if the first thing you do after getting a 'Left' is just raise an exception/halt the program, then i think it's fine to just have the invalid-data be an Exception too, for practical/pragmatic reasons
romano 2017-02-01 20:28:12
jle`, that's what i'm doing now :)
dram_phone 2017-02-01 20:28:24
romano: so normally it *should never occur* right?
jle` 2017-02-01 20:28:35
i wouldn't be happy about it but i wouldn't dwell on it if it's just a minor situation like this
ski 2017-02-01 20:28:53
dram_phone : "use site" being each individual call to a library operation that might signal/raise/throw the condition/exception ? or just some site(s) that's a bit up the call tree from those calls ?
dram_phone 2017-02-01 20:29:42
I mean, for, say:
jle` 2017-02-01 20:29:44
i think it *should* be an Either that is handled, for scalability/maintainability, but if those aren't major issues then who cares right
dram_phone 2017-02-01 20:29:50
:t Data.Map.Lazy.lookup
lambdabot 2017-02-01 20:29:52
Ord k => k -> M.Map k a -> Maybe a
ski 2017-02-01 20:30:07
dram_phone : *nod*
dram_phone 2017-02-01 20:30:07
imagine that the Maybe isn't there
jle` 2017-02-01 20:30:22
:t flip (Data.Map.Lazy.!)
lambdabot 2017-02-01 20:30:24
Ord k => k -> M.Map k c -> c
ski 2017-02-01 20:30:43
in this case, you often (not always) want to handle the failure situation right away after the call to `lookup'
dram_phone 2017-02-01 20:30:43
Yeah imagine that *all* you have is that
romano 2017-02-01 20:31:01
jle`, i thought of IO (Either e a) but as far as i understand it's not possible to sequence these in the monadic sense
dram_phone 2017-02-01 20:31:05
'key not found' is often normal
jle` 2017-02-01 20:31:14
romano: you can sequence them by using the ExceptT newtype wrapper
jle` 2017-02-01 20:31:47
you might be familiar with other newtype wrappers that give values neat instances, like Sum, Any, Product, First, etc.
dram_phone 2017-02-01 20:31:50
ski: Did I get the point across?
ski 2017-02-01 20:32:02
jle` : especially if you want to be able to present the exception in different ways, depending on the UI, or localization .. or sometimes maybe do some symbolic processing of them
jle` 2017-02-01 20:32:24
was that meant for dram_phone
romano 2017-02-01 20:33:21
ok, i'll have another look at exceptT then. thanks for the input guys!
dram_phone 2017-02-01 20:33:34
All non-internal error messages should be ADTs
ski 2017-02-01 20:34:09
jle` : no, it was a response to "i think it *should* be an Either that is handled, for scalability/maintainability, ..."
jle` 2017-02-01 20:34:21
ah, yes :)
erikd 2017-02-01 20:40:02
is it possible to have a cabal project where an executable in the project generates Haskell code which is use to build the library?
ski 2017-02-01 20:40:15
dram_phone : hm, i'm not sure. i think either you're talking about a situation where "it shouldn't happen" that you access a map with a non-existent key; or you're talking about the difference between on the one hand only using `Maybe'/`Either' to communicate failure to the caller, which immediately handles the failure, and on the other hand, using `Maybe'/`Either'/`ExceptT' (or perhaps `Control.Exception' ?) to propagate failure until such time that you se
ski 2017-02-01 20:40:30
hrm, cut off near ".., and on the other hand, using `Maybe'/`Either'/`ExceptT' (or perhaps `Control.Exception' ?) to propagate failure until such time that you see fit to handle/catch it -- but i'm not sure which"
dram_phone 2017-02-01 20:42:57
Hmm let me see
dram_phone 2017-02-01 20:43:19
You do know 'if' right? If you're using exceptions like 'if's you're doing it wrong
dram_phone 2017-02-01 20:44:03
That's what I mean by 'normal'
dram_phone 2017-02-01 20:44:29
The 'not found' thing is actually in sort of a gray area
ski 2017-02-01 20:44:41
mniip : anyway, in the internal language, variable terms gets translated to a projection out of the context, treated as a product type (by removing the variable names, and replacing `,'s by `*', so the context `(f : A * B -> C,x : A),y : B' becomes the product type `((A * B -> C) * A) * B')
